theorem :: GROUP_2:5

for G being Group holds ({} the carrier of G) " = {}