:: deftheorem Def10 defines /\ GROUP_2:def 10 :
for G being Group
for H1, H2 being Subgroup of G
for b₄ being strict Subgroup of G holds
( b₄ = H1 /\ H2 iff the carrier of b₄ = (carr H1) /\ (carr H2) );