diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 2b595d700fe63f109c7d8245b0535af199028430..d271c2c7a0a4f4e7ae533d400008a259e064021b 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -119,8 +119,7 @@ Section bi_mixin.
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
       <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);
 
-    (* In the ordered RA model: [core x ≼ core (x ⋅ y)].
-       Note that this implies that the core is monotone. *)
+    (* In the ordered RA model: [core x ≼ core (x ⋅ y)]. *)
     bi_mixin_persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P;
     (* In the ordered RA model: [x â‹… core x = core x]. *)
     bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;