:: deftheorem Def7 defines Phi GROUP_4:def 7 :
for G being Group
for b₂ being strict Subgroup of G holds
( ( ex H being strict Subgroup of G st H is maximal implies ( b₂ = Phi G iff 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 ( b₂ = Phi G iff b₂ = multMagma(# the carrier of G, the multF of G #) ) ) );