:: deftheorem Def7 defines (0). GROUP_1A:def 17 :
for G being addGroup
for b₂ being strict Subgroup of G holds
( b₂ = (0). G iff the carrier of b₂ = {(0_ G)} );