let G be Group; :: thesis: for a being Element of G
for G being Group st ex H being strict Subgroup of G st H is maximal holds
( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
let a be Element of G; :: thesis: for G being Group st ex H being strict Subgroup of G st H is maximal holds
( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
let G be Group; :: thesis: ( ex H being strict Subgroup of G st H is maximal implies ( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H ) )
assume A1: ex H being strict Subgroup of G st H is maximal ; :: thesis: ( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
set X = { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal ) } ;
thus ( a in Phi G implies for H being strict Subgroup of G st H is maximal holds
a in H ) :: thesis: ( ( for H being strict Subgroup of G st H is maximal holds
a in H ) implies a in Phi G )

proof

assume a in Phi G ; :: thesis: for H being strict Subgroup of G st H is maximal holds
a in H
then a in the carrier of (Phi G) by STRUCT_0:def 5;
then A2: a in meet { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal ) } by A1, Def8;
let H be strict Subgroup of G; :: thesis: ( H is maximal implies a in H )
assume H is maximal ; :: thesis: a in H
then carr H in { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal ) } ;
then a in carr H by A2, SETFAM_1:def 1;
hence a in H by STRUCT_0:def 5; :: thesis: verum

end;

consider H being strict Subgroup of G such that
A3: H is maximal by A1;
A4: carr H in { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal ) } by A3;
assume A5: for H being strict Subgroup of G st H is maximal holds
a in H ; :: thesis: a in Phi G

now

let Y be set ; :: thesis: ( Y in { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal ) } implies a in Y )
assume Y in { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal ) } ; :: thesis: a in Y
then consider A being Subset of G such that
A6: Y = A and
A7: ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal ) ;
consider H being strict Subgroup of G such that
A8: ( A = the carrier of H & H is maximal ) by A7;
( A = carr H & a in H ) by A5, A8;
hence a in Y by A6, STRUCT_0:def 5; :: thesis: verum

end;

then a in meet { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal ) } by A4, SETFAM_1:def 1;
then a in the carrier of (Phi G) by A1, Def8;
hence a in Phi G by STRUCT_0:def 5; :: thesis: verum