defpred S₁[ Subgroup of G] means $1 is maximal ;

now :: thesis:

per cases ;

suppose A1: ex H being strict Subgroup of G st S₁[H] ; :: thesis:

ex H being strict Subgroup of G st the carrier of H = meet { A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & S₁[K] ) } from GROUP_4:sch 1(A1);
hence ( ( ex H being strict Subgroup of G st H is maximal implies ex b₁ being strict Subgroup of G st the carrier of b₁ = meet { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal ) } ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b₁ being strict Subgroup of G st b₁ = multMagma(# the carrier of G, the multF of G #) ) ) by A1; :: thesis:

end;

suppose A2: for H being strict Subgroup of G holds not H is maximal ; :: thesis:

(Omega). G = multMagma(# the carrier of G, the multF of G #) ;
hence ( ( ex H being strict Subgroup of G st H is maximal implies ex b₁ being strict Subgroup of G st the carrier of b₁ = meet { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal ) } ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b₁ being strict Subgroup of G st b₁ = multMagma(# the carrier of G, the multF of G #) ) ) by A2; :: thesis:

end;

end;

end;

hence ( ( ex H being strict Subgroup of G st H is maximal implies ex b₁ being strict Subgroup of G st the carrier of b₁ = meet { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal ) } ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b₁ being strict Subgroup of G st b₁ = multMagma(# the carrier of G, the multF of G #) ) ) ; :: thesis: