let G be Group; :: thesis: for A being Subset of G holds gr A = gr (A \ {(1_ G)})
let A be Subset of G; :: thesis: gr A = gr (A \ {(1_ G)})
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 ) } ;
set Y = { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) } ;
A1: { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) } = { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) }
proof
thus { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) } c= { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) } :: according to XBOOLE_0:def 10 :: thesis: { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) } c= { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x 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 ) } or x in { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) } )
assume x 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: x in { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) }
then consider B being Subset of G such that
A2: x = B and
A3: ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) ;
consider H being strict Subgroup of G such that
A4: B = the carrier of H and
A5: A c= carr H by A3;
A \ {(1_ G)} c= A by XBOOLE_1:36;
then A \ {(1_ G)} c= carr H by A5;
hence x in { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) } by A2, A4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) } or x 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 ) } )
assume x in { C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H ) } ; :: thesis: x 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 consider B being Subset of G such that
A6: x = B and
A7: ex H being strict Subgroup of G st
( B = the carrier of H & A \ {(1_ G)} c= carr H ) ;
consider H being strict Subgroup of G such that
A8: B = the carrier of H and
A9: A \ {(1_ G)} c= carr H by A7;
1_ G in H by GROUP_2:46;
then 1_ G in carr H by STRUCT_0:def 5;
then {(1_ G)} c= carr H by ZFMISC_1:31;
then A10: (A \ {(1_ G)}) \/ {(1_ G)} c= carr H by A9, XBOOLE_1:8;
now :: thesis: A c= carr H
end;
hence x 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 A6, A8; :: thesis: verum
end;
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 Th34
.= the carrier of (gr (A \ {(1_ G)})) by A1, Th34 ;
hence gr A = gr (A \ {(1_ G)}) by GROUP_2:59; :: thesis: verum