let G be Group; :: thesis: for H being finite strict Subgroup of G st card H = 1 holds
H = (1). G
let H be finite strict Subgroup of G; :: thesis: ( card H = 1 implies H = (1). G )
assume card H = 1 ; :: thesis: H = (1). G
then consider x being object such that
A1: the carrier of H = {x} by CARD_2:42;
1_ G in H by Th46;
then 1_ G in the carrier of H ;
then x = 1_ G by A1, TARSKI:def 1;
hence H = (1). G by A1, Def7; :: thesis: verum