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