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

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