let G be Group; :: thesis: for A being Subset of G holds the carrier of (gr A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) }
let A be Subset of G; :: thesis: the carrier of (gr A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) }
defpred S1[ Subgroup of G] means A c= carr $1;
set X = { B where B is Subset of G : ex H being strict Subgroup 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 Subgroup of G st
( 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 Subgroup 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 Subgroup 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 Subgroup of G st
( B = the carrier of H & A c= carr H ) ) ;
hence A c= Y ; :: thesis: verum
end;
the carrier of ((Omega). G) = carr ((Omega). G) ;
then A2: ex H being strict Subgroup of G st S1[H] ;
consider H being strict Subgroup of G such that
A3: the carrier of H = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S1[H] ) } from GROUP_4:sch 1(A2);
A4: now :: thesis: for H1 being strict Subgroup of G st A c= the carrier of H1 holds
H is Subgroup of H1
let H1 be strict Subgroup of G; :: thesis: ( A c= the carrier of H1 implies H is Subgroup of H1 )
A5: the carrier of H1 = carr H1 ;
assume A c= the carrier of H1 ; :: thesis: H is Subgroup of H1
then the carrier of H1 in { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) } by A5;
hence H is Subgroup of H1 by A3, GROUP_2:57, SETFAM_1:3; :: thesis: verum
end;
carr ((Omega). G) in { B where B is Subset of G : ex H being strict Subgroup of G st
( 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 (gr A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) } by A3, A4, Def4; :: thesis: verum