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

now :: thesis: ( ( 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 #) ) )

per cases ( ex H being strict Subgroup of G st S₁[H] or for H being strict Subgroup of G holds not H is maximal ) ;

suppose A1: ex H being strict Subgroup of G st S₁[H] ; :: thesis: ( ( 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 #) ) )

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: verum

end;

suppose A2: for H being strict Subgroup of G holds not H is maximal ; :: thesis: ( ( 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 #) ) )

(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: verum

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: verum