let G be Group; :: thesis: gr ({} the carrier of G) = (1). G
A1: {} the carrier of G c= the carrier of ((1). G) by XBOOLE_1:2;
for H being strict Subgroup of G st {} the carrier of G c= the carrier of H holds
(1). G is Subgroup of H by GROUP_2:77;
hence gr ({} the carrier of G) = (1). G by A1, Def5; :: thesis: verum