theorem :: GROUP_4:30

for G being Group holds gr ({} the carrier of G) = (1). G