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 ) )
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 ) } ;
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 )
then consider H being strict Subgroup of G such that
A2: H 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 A3: 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, Def7;
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 A3, SETFAM_1:def 1;
hence a in H by STRUCT_0:def 5; :: thesis: verum

end;

assume A4: for H being strict Subgroup of G st H is maximal holds
a in H ; :: thesis: a in Phi G

A5: now :: thesis: for Y being set st 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 ) } holds
a in Y

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 and
A9: H is maximal by A7;
a in H by A4, A9;
hence a in Y by A6, A8, STRUCT_0:def 5; :: thesis: verum

end;

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 A2;
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 A5, SETFAM_1:def 1;
then a in the carrier of (Phi G) by A1, Def7;
hence a in Phi G by STRUCT_0:def 5; :: thesis: verum