let G be Group; :: thesis: gr ({} the carrier of G) = (1). G
( {} the carrier of G c= the carrier of ((1). G) & ( 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, XBOOLE_1:2;
hence gr ({} the carrier of G) = (1). G by Def5; :: thesis: verum