:: deftheorem defines + GROUP_1A:def 24 :
for G being addGroup
for H being Subgroup of G
for a being Element of G holds H + a = (carr H) + a;