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