:: deftheorem Def7 defines (1). GROUP_2:def 7 :
for G being Group
for b₂ being strict Subgroup of G holds
( b₂ = (1). G iff the carrier of b₂ = {(1_ G)} );