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:65;
hence gr ({} the carrier of G) = (1). G by Def4; :: thesis: verum