diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 4bc0972888ecb3dee7cfecf3e0dabf3315272837..2b595d700fe63f109c7d8245b0535af199028430 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -110,7 +110,8 @@ Section bi_mixin.
     (* In the ordered RA model: `core` is idempotent *)
     bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
 
-    (* In the ordered RA model: `ε ≼ core x` *)
+    (* In the ordered RA model: `core ε = ε`, which implies together with
+       monotonicity that `ε ≼ core x`. *)
     bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :