:: deftheorem defines maximal GROUP_4:def 6 :
for G being Group
for H being Subgroup of G holds
( H is maximal iff ( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds
K = multMagma(# the carrier of G, the multF of G #) ) ) );