:: deftheorem Def6A defines * GROUP_1A:def 34 :
for G being addGroup
for H being Subgroup of G
for a being Element of G
for b₄ being strict Subgroup of G holds
( b₄ = H * a iff the carrier of b₄ = (carr H) * a );