:: deftheorem Def8 defines (1). GROUP_9:def 8 :
for O being set
for G being GroupWithOperators of O
for b₃ being strict StableSubgroup of G holds
( b₃ = (1). G iff the carrier of b₃ = {(1_ G)} );