:: deftheorem Def11 defines SubMeet GROUP_4:def 11 :
for G being Group
for b₂ being BinOp of (Subgroups G) holds
( b₂ = SubMeet G iff for H1, H2 being strict Subgroup of G holds b₂ . (H1,H2) = H1 /\ H2 );