:: deftheorem defines + GROUP_1A:def 21 :
for G being addGroup
for H being Subgroup of G
for A being Subset of G holds A + H = A + (carr H);