typos

set.mm

@@ -15574,10 +15574,10 @@ only postulated (that is, axiomatic) rule of inference of predicate
   set, ~ ax-pr postulates the existence of at least two sets, and finally
   ~ ax-inf postulates the existence of an infinite number of sets. It is
   nevertheless interesting to shortly develop this case because the results are
-  exactly meeting our intuition. Every universally quantified wwf is provably
-  true, and every existentially quantified wwf is provably false. Otherwise,
+  exactly meeting our intuition. Every universally quantified wff is provably
+  true, and every existentially quantified wff is provably false. Otherwise,
   nothing can be said. Reciprocally, in the case that every universally
-  quantified wwf is true, then ~ ax-6 is negated, but ~ ax-gen , ~ ax-4 ,
+  quantified wff is true, then ~ ax-6 is negated, but ~ ax-gen , ~ ax-4 ,
   ~ ax-5 , ~ ax-10 , ~ ax-11 , ~ ax-12 and ~ ax-13 are automatically true, and
   so are also every universal quantification of ~ ax-7 , ~ ax-8 and ~ ax-9 .
 $)
@@ -15587,13 +15587,13 @@ only postulated (that is, axiomatic) rule of inference of predicate
   nax6ex $p |- ( -. E. x T. -> -. E. x ph ) $=
     ( wex wtru trud eximi con3i ) ABCDBCADBAEFG $.
 
-  $( In an empty domain the for-all operator always holds, even when applied to
-     a false expression.  This theorem actually shows that ~ ax-5 is provable
-     there.  Also we cannot assume that ~ sp generally holds, except of course
-     in the form of ~ sptruw .  Without the support of an ~ sp like theorem it
-     seems difficult, if not impossible, to arrive at a theorem allowing to
-     change the bounded variable in the antecedent.  Additional axioms need to
-     be postulated to further strengthen this result.
+  $( In an empty logical domain the for-all operator always holds, even when
+     applied to a false expression.  This theorem actually shows that ~ ax-5 is
+     provable there.  Also we cannot assume that ~ sp generally holds, except
+     of course in the form of ~ sptruw .  Without the support of an ~ sp like
+     theorem it seems difficult, if not impossible, to arrive at a theorem
+     allowing to change the bounded variable in the antecedent.  Additional
+     axioms need to be postulated to further strengthen this result.
 
      A consequence of this result is that ` E. x ph ` is not true for any
      ` ph ` .  In particular, ` E* x ph ` does not hold either, a somewhat