:: deftheorem Def10 defines /\ GROUP_1A:def 20 :
for G being addGroup
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) );