theorem :: GROUP_2:6

for G being Group holds ([#] the carrier of G) " = the carrier of G