diff --git a/set.mm b/set.mm
index cba01bb92..1d3e86d27 100644
--- a/set.mm
+++ b/set.mm
@@ -127694,13 +127694,13 @@ this axiom (with the defined operation in place of ` + ` ) follows as a
   $( $j restatement 'ax-addf' of 'axaddf'; $)
 
   $( Multiplication is an operation on the complex numbers.  This deprecated
-     axiom is provided for historical compatibility but is not a bona fide
-     axiom for complex numbers (independent of set theory) since it cannot be
-     interpreted as a first-order or second-order statement (see
-     ~ https://us.metamath.org/downloads/schmidt-cnaxioms.pdf ).  It may be
-     deleted in the future and should be avoided for new theorems.  Instead,
-     the less specific ~ ax-mulcl should be used.  Note that uses of ~ ax-mulf
-     can be eliminated by using the defined operation
+     axiom is provided for historical compatibility.  However, while Metamath
+     can handle it, it cannot be interpreted as a first-order or second-order
+     statement.  We generally prefer simpler statements (see
+     ~ https://us.metamath.org/downloads/schmidt-cnaxioms.pdf ).  This
+     deprecated axiom may be deleted in the future and should be avoided for
+     new theorems.  Instead, the less specific ~ ax-mulcl should be used.  Note
+     that uses of ~ ax-mulf can be eliminated by using the defined operation
      ` ( x e. CC , y e. CC |-> ( x x. y ) ) ` in place of ` x. ` , from which
      this axiom (with the defined operation in place of ` x. ` ) follows as a
      theorem.