:: deftheorem defines carr GROUP_1A:def 19 :
for G being addGroup
for H being Subgroup of G holds carr H = the carrier of H;