let O be set ; :: thesis: for G being GroupWithOperators of O

for A being Subset of G holds the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) }

let G be GroupWithOperators of O; :: thesis: for A being Subset of G holds the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) }

let A be Subset of G; :: thesis: the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) }

defpred S_{1}[ StableSubgroup of G] means A c= carr $1;

set X = { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } ;

then A2: ex H being strict StableSubgroup of G st S_{1}[H]
;

consider H being strict StableSubgroup of G such that

A3: the carrier of H = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & S_{1}[H] ) }
from GROUP_9:sch 1(A2);

( B = the carrier of H & A c= carr H ) } ;

then A c= the carrier of H by A3, A1, SETFAM_1:5;

hence the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } by A3, A4, Def26; :: thesis: verum

for A being Subset of G holds the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) }

let G be GroupWithOperators of O; :: thesis: for A being Subset of G holds the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) }

let A be Subset of G; :: thesis: the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) }

defpred S

set X = { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } ;

A1: now :: thesis: for Y being set st Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } holds

A c= Y

the carrier of ((Omega). G) = carr ((Omega). G)
;( B = the carrier of H & A c= carr H ) } holds

A c= Y

let Y be set ; :: thesis: ( Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } implies A c= Y )

assume Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } ; :: thesis: A c= Y

then ex B being Subset of G st

( Y = B & ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) ) ;

hence A c= Y ; :: thesis: verum

end;( B = the carrier of H & A c= carr H ) } implies A c= Y )

assume Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } ; :: thesis: A c= Y

then ex B being Subset of G st

( Y = B & ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) ) ;

hence A c= Y ; :: thesis: verum

then A2: ex H being strict StableSubgroup of G st S

consider H being strict StableSubgroup of G such that

A3: the carrier of H = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & S

A4: now :: thesis: for H1 being strict StableSubgroup of G st A c= the carrier of H1 holds

H is StableSubgroup of H1

carr ((Omega). G) in { B where B is Subset of G : ex H being strict StableSubgroup of G st H is StableSubgroup of H1

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

A5: 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 { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } by A5;

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

end;A5: 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 { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } by A5;

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

( B = the carrier of H & A c= carr H ) } ;

then A c= the carrier of H by A3, A1, SETFAM_1:5;

hence the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & A c= carr H ) } by A3, A4, Def26; :: thesis: verum