theorem :: GROUP_1A:52

for G being addGroup holds - ([#] the carrier of G) = the carrier of G