diff --git a/set.mm b/set.mm
index f0c9ab553b..864cb7dc1f 100644
--- a/set.mm
+++ b/set.mm
@@ -431159,6 +431159,16 @@ be applied for new theorems (formerly, the class and wff variables
        ~ mmtheorems32.html#mm3146s also describes the
        metatheorem that underlies this.
 
+       <p>You should read any statement starting with ` |- `
+       and having one or more unbound set variable(s) as universally
+       quantified over those
+       variables. So if you state ` |- 0 < k ` , say as a postulate,
+       that's saying " ` 0 < k ` is derivable in the empty context"
+       which is a strong statement,
+       equivalent to ` A. k 0 < k ` , which without further context is false.
+       The same is not true for class variables (e.g., ` 0 < K ` is typically
+       safe to postulate).
+
        <p><b>Additional rules for definitions</b>
 
        <p>Standard Metamath verifiers do not distinguish between axioms and