Reformatting

set.mm

@@ -217885,8 +217885,8 @@ everywhere defined internal operation (see ~ mndcl ), whose operation is
        (Note that we must add the condition that the zero of the parent monoid
        is actually contained in the submonoid, because it is possible to have
        "subsets that are monoids" which are not submonoids because they have a
-       different identity element. See, for example, ~ smndex1mnd and
-       ~ smndex1n0mnd )  (Contributed by Mario Carneiro, 10-Jan-2015.) $)
+       different identity element.  See, for example, ~ smndex1mnd and
+       ~ smndex1n0mnd ) (Contributed by Mario Carneiro, 10-Jan-2015.) $)
     submnd0 $p |- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) ->
       .0. = ( 0g ` H ) ) $=
       ( vx cmnd wcel wa cbs cfv cplusg eqid wceq co cvv oveqd ressbas2 ad2antrl