theorem :: GROUP_1A:52
for G being addGroup holds - ([#] the carrier of G) = the carrier of G