defpred S₁[ set ] means ex H being strict multSubmagma of M st
( $1 = the carrier of H & A c= $1 );
consider X being set such that
A1: for Y being set holds
( Y in X iff ( Y in bool the carrier of M & S₁[Y] ) ) from XFAMILY:sch 1();
set F = id X;
set A1 = meet (id X);
for x being set st x in dom (id X) holds
(id X) . x is stable Subset of M

proof

let x be set ; :: thesis: ( x in dom (id X) implies (id X) . x is stable Subset of M )
assume A2: x in dom (id X) ; :: thesis: (id X) . x is stable Subset of M
then ( x in bool the carrier of M & S₁[x] ) by A1;
hence (id X) . x is stable Subset of M by A2, FUNCT_1:18; :: thesis: verum

end;

then reconsider A1 = meet (id X) as stable Subset of M by Th9;
set N1 = multMagma(# A1,(the_mult_induced_by A1) #);
take multMagma(# A1,(the_mult_induced_by A1) #) ; :: thesis: ( multMagma(# A1,(the_mult_induced_by A1) #) is strict multSubmagma of M & A c= the carrier of multMagma(# A1,(the_mult_induced_by A1) #) & ( for N being strict multSubmagma of M st A c= the carrier of N holds
multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N ) )

per cases ( X = {} or X <> {} ) ;

suppose A3: X = {} ; :: thesis: ( multMagma(# A1,(the_mult_induced_by A1) #) is strict multSubmagma of M & A c= the carrier of multMagma(# A1,(the_mult_induced_by A1) #) & ( for N being strict multSubmagma of M st A c= the carrier of N holds
multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N ) )

A4: the carrier of M in bool the carrier of M by ZFMISC_1:def 1;
ex H being strict multSubmagma of M st
( the carrier of M = the carrier of H & A c= the carrier of M )

proof

the multF of M = the multF of M | [: the carrier of M, the carrier of M:] ;
then the multF of M = the multF of M || the carrier of M by REALSET1:def 2;
then reconsider H = multMagma(# the carrier of M, the multF of M #) as strict multSubmagma of M by Def9;
take H ; :: thesis: ( the carrier of M = the carrier of H & A c= the carrier of M )
thus the carrier of M = the carrier of H ; :: thesis: A c= the carrier of M
thus A c= the carrier of M ; :: thesis: verum

end;

hence ( multMagma(# A1,(the_mult_induced_by A1) #) is strict multSubmagma of M & A c= the carrier of multMagma(# A1,(the_mult_induced_by A1) #) & ( for N being strict multSubmagma of M st A c= the carrier of N holds
multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N ) ) by A3, A4, A1; :: thesis: verum

end;

suppose A5: X <> {} ; :: thesis: ( multMagma(# A1,(the_mult_induced_by A1) #) is strict multSubmagma of M & A c= the carrier of multMagma(# A1,(the_mult_induced_by A1) #) & ( for N being strict multSubmagma of M st A c= the carrier of N holds
multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N ) )

A6: for x being object st x in A holds
x in A1

proof

let x be object ; :: thesis: ( x in A implies x in A1 )
assume A7: x in A ; :: thesis: x in A1
for Y being set st Y in X holds
x in Y

proof

let Y be set ; :: thesis: ( Y in X implies x in Y )
assume Y in X ; :: thesis: x in Y
then consider H being strict multSubmagma of M such that
A8: ( Y = the carrier of H & A c= Y ) by A1;
thus x in Y by A8, A7; :: thesis: verum

end;

then x in meet X by A5, SETFAM_1:def 1;
then x in meet (rng (id X)) ;
hence x in A1 by FUNCT_6:def 4; :: thesis: verum

end;

for N being strict multSubmagma of M st A c= the carrier of N holds
multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N

proof

let N be strict multSubmagma of M; :: thesis: ( A c= the carrier of N implies multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N )
assume A9: A c= the carrier of N ; :: thesis: multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N
for x being object st x in the carrier of multMagma(# A1,(the_mult_induced_by A1) #) holds
x in the carrier of N

proof

let x be object ; :: thesis: ( x in the carrier of multMagma(# A1,(the_mult_induced_by A1) #) implies x in the carrier of N )
assume x in the carrier of multMagma(# A1,(the_mult_induced_by A1) #) ; :: thesis: x in the carrier of N
then x in meet (rng (id X)) by FUNCT_6:def 4;
then A10: x in meet X ;
the carrier of N c= the carrier of M by Def9;
then the carrier of N in X by A1, A9;
hence x in the carrier of N by A10, SETFAM_1:def 1; :: thesis: verum

end;

then A11: the carrier of multMagma(# A1,(the_mult_induced_by A1) #) c= the carrier of N ;
A12: the multF of M | [: the carrier of N, the carrier of N:] = the multF of M || the carrier of N by REALSET1:def 2
.= the multF of N by Def9 ;
the multF of multMagma(# A1,(the_mult_induced_by A1) #) = the multF of M | [: the carrier of multMagma(# A1,(the_mult_induced_by A1) #), the carrier of multMagma(# A1,(the_mult_induced_by A1) #):] by REALSET1:def 2
.= ( the multF of M | [: the carrier of N, the carrier of N:]) | [: the carrier of multMagma(# A1,(the_mult_induced_by A1) #), the carrier of multMagma(# A1,(the_mult_induced_by A1) #):] by A11, RELAT_1:74, ZFMISC_1:96
.= the multF of N || the carrier of multMagma(# A1,(the_mult_induced_by A1) #) by A12, REALSET1:def 2 ;
hence multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N by A11, Def9; :: thesis: verum

end;

hence ( multMagma(# A1,(the_mult_induced_by A1) #) is strict multSubmagma of M & A c= the carrier of multMagma(# A1,(the_mult_induced_by A1) #) & ( for N being strict multSubmagma of M st A c= the carrier of N holds
multMagma(# A1,(the_mult_induced_by A1) #) is multSubmagma of N ) ) by A6, Def9; :: thesis: verum

end;

end;