:: deftheorem defines carr GROUP_2:def 9 :
for G being Group
for H being Subgroup of G holds carr H = the carrier of H;