Rewrap

set.mm

@@ -655015,8 +655015,8 @@ collection and union ( ~ mnuop3d ), from which closure under pairing
        limit to an inequality cf. ~ https://math.stackexchange.com/q/2215191 ,
        and how to use ~ r19.29a in a similar fashion to Mario Carneiro's proof
        sketch with ~ rexlimdva at
-       ~ https://groups.google.com/g/metamath/c/2RPikOiXLMo .)
-       (Contributed by Steve Rodriguez, 28-Feb-2020.) $)
+       ~ https://groups.google.com/g/metamath/c/2RPikOiXLMo .)  (Contributed by
+       Steve Rodriguez, 28-Feb-2020.) $)
     cvgdvgrat $p |- ( ph -> ( L < 1 <-> seq M ( + , F ) e. dom ~~> ) ) $=
       ( c1 vr vn vi clt wbr caddc cseq cli cdm wcel wa cioo co wral cv cfv cabs
       cmul cle cuz eqid cr elioore ad3antlr w3a cxr wb cz syl6eleq eluzelz cdiv