defpred S_{1}[ set ] means ex H being strict StableSubgroup of G st

( $1 = carr 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 G & S_{1}[Y] ) )
from XFAMILY:sch 1();

set M = meet X;

A2: carr ((Omega). G) = the carrier of ((Omega). G) ;

then A3: X <> {} by A1;

A4: the carrier of G in X by A1, A2;

A5: meet X c= the carrier of G by A4, SETFAM_1:def 1;

reconsider M = meet X as Subset of G by A5;

A21: the carrier of H = M by A7, A12, A8, Lm14;

take H ; :: thesis: ( A c= the carrier of H & ( for H being strict StableSubgroup of G st A c= the carrier of H holds

H is StableSubgroup of H ) )

H is StableSubgroup of H

let H1 be strict StableSubgroup of G; :: thesis: ( A c= the carrier of H1 implies H is StableSubgroup of H1 )

A22: the carrier of H1 = carr H1 ;

assume A c= the carrier of H1 ; :: thesis: H is StableSubgroup of H1

then the carrier of H1 in X by A1, A22;

hence H is StableSubgroup of H1 by A21, Lm20, SETFAM_1:3; :: thesis: verum

( $1 = carr 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 G & S

set M = meet X;

A2: carr ((Omega). G) = the carrier of ((Omega). G) ;

then A3: X <> {} by A1;

A4: the carrier of G in X by A1, A2;

A5: meet X c= the carrier of G by A4, SETFAM_1:def 1;

now :: thesis: for Y being set st Y in X holds

1_ G in Y

then A7:
meet X <> {}
by A3, SETFAM_1:def 1;1_ G in Y

let Y be set ; :: thesis: ( Y in X implies 1_ G in Y )

assume Y in X ; :: thesis: 1_ G in Y

then consider H being strict StableSubgroup of G such that

A6: Y = carr H and

A c= Y by A1;

1_ G in H by Lm17;

hence 1_ G in Y by A6, STRUCT_0:def 5; :: thesis: verum

end;assume Y in X ; :: thesis: 1_ G in Y

then consider H being strict StableSubgroup of G such that

A6: Y = carr H and

A c= Y by A1;

1_ G in H by Lm17;

hence 1_ G in Y by A6, STRUCT_0:def 5; :: thesis: verum

reconsider M = meet X as Subset of G by A5;

A8: now :: thesis: for o being Element of O

for a being Element of G st a in M holds

(G ^ o) . a in M

for a being Element of G st a in M holds

(G ^ o) . a in M

let o be Element of O; :: thesis: for a being Element of G st a in M holds

(G ^ o) . a in M

let a be Element of G; :: thesis: ( a in M implies (G ^ o) . a in M )

assume A9: a in M ; :: thesis: (G ^ o) . a in M

end;(G ^ o) . a in M

let a be Element of G; :: thesis: ( a in M implies (G ^ o) . a in M )

assume A9: a in M ; :: thesis: (G ^ o) . a in M

now :: thesis: for Y being set st Y in X holds

(G ^ o) . a in Y

hence
(G ^ o) . a in M
by A3, SETFAM_1:def 1; :: thesis: verum(G ^ o) . a in Y

let Y be set ; :: thesis: ( Y in X implies (G ^ o) . a in Y )

assume A10: Y in X ; :: thesis: (G ^ o) . a in Y

then consider H being strict StableSubgroup of G such that

A11: Y = carr H and

A c= Y by A1;

a in carr H by A9, A10, A11, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then (G ^ o) . a in H by Lm9;

hence (G ^ o) . a in Y by A11, STRUCT_0:def 5; :: thesis: verum

end;assume A10: Y in X ; :: thesis: (G ^ o) . a in Y

then consider H being strict StableSubgroup of G such that

A11: Y = carr H and

A c= Y by A1;

a in carr H by A9, A10, A11, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then (G ^ o) . a in H by Lm9;

hence (G ^ o) . a in Y by A11, STRUCT_0:def 5; :: thesis: verum

A12: now :: thesis: for a, b being Element of G st a in M & b in M holds

a * b in M

a * b in M

let a, b be Element of G; :: thesis: ( a in M & b in M implies a * b in M )

assume that

A13: a in M and

A14: b in M ; :: thesis: a * b in M

end;assume that

A13: a in M and

A14: b in M ; :: thesis: a * b in M

now :: thesis: for Y being set st Y in X holds

a * b in Y

hence
a * b in M
by A3, SETFAM_1:def 1; :: thesis: veruma * b in Y

let Y be set ; :: thesis: ( Y in X implies a * b in Y )

assume A15: Y in X ; :: thesis: a * b in Y

then consider H being strict StableSubgroup of G such that

A16: Y = carr H and

A c= Y by A1;

b in carr H by A14, A15, A16, SETFAM_1:def 1;

then A17: b in H by STRUCT_0:def 5;

a in carr H by A13, A15, A16, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a * b in H by A17, Lm18;

hence a * b in Y by A16, STRUCT_0:def 5; :: thesis: verum

end;assume A15: Y in X ; :: thesis: a * b in Y

then consider H being strict StableSubgroup of G such that

A16: Y = carr H and

A c= Y by A1;

b in carr H by A14, A15, A16, SETFAM_1:def 1;

then A17: b in H by STRUCT_0:def 5;

a in carr H by A13, A15, A16, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a * b in H by A17, Lm18;

hence a * b in Y by A16, STRUCT_0:def 5; :: thesis: verum

now :: thesis: for a being Element of G st a in M holds

a " in M

then consider H being strict StableSubgroup of G such that a " in M

let a be Element of G; :: thesis: ( a in M implies a " in M )

assume A18: a in M ; :: thesis: a " in M

end;assume A18: a in M ; :: thesis: a " in M

now :: thesis: for Y being set st Y in X holds

a " in Y

hence
a " in M
by A3, SETFAM_1:def 1; :: thesis: veruma " in Y

let Y be set ; :: thesis: ( Y in X implies a " in Y )

assume A19: Y in X ; :: thesis: a " in Y

then consider H being strict StableSubgroup of G such that

A20: Y = carr H and

A c= Y by A1;

a in carr H by A18, A19, A20, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a " in H by Lm19;

hence a " in Y by A20, STRUCT_0:def 5; :: thesis: verum

end;assume A19: Y in X ; :: thesis: a " in Y

then consider H being strict StableSubgroup of G such that

A20: Y = carr H and

A c= Y by A1;

a in carr H by A18, A19, A20, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a " in H by Lm19;

hence a " in Y by A20, STRUCT_0:def 5; :: thesis: verum

A21: the carrier of H = M by A7, A12, A8, Lm14;

take H ; :: thesis: ( A c= the carrier of H & ( for H being strict StableSubgroup of G st A c= the carrier of H holds

H is StableSubgroup of H ) )

now :: thesis: for Y being set st Y in X holds

A c= Y

hence
A c= the carrier of H
by A3, A21, SETFAM_1:5; :: thesis: for H being strict StableSubgroup of G st A c= the carrier of H holds A c= Y

let Y be set ; :: thesis: ( Y in X implies A c= Y )

assume Y in X ; :: thesis: A c= Y

then ex H being strict StableSubgroup of G st

( Y = carr H & A c= Y ) by A1;

hence A c= Y ; :: thesis: verum

end;assume Y in X ; :: thesis: A c= Y

then ex H being strict StableSubgroup of G st

( Y = carr H & A c= Y ) by A1;

hence A c= Y ; :: thesis: verum

H is StableSubgroup of H

let H1 be strict StableSubgroup of G; :: thesis: ( A c= the carrier of H1 implies H is StableSubgroup of H1 )

A22: the carrier of H1 = carr H1 ;

assume A c= the carrier of H1 ; :: thesis: H is StableSubgroup of H1

then the carrier of H1 in X by A1, A22;

hence H is StableSubgroup of H1 by A21, Lm20, SETFAM_1:3; :: thesis: verum