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 set such that
A1: the carrier of H = {x} by CARD_2:60;
1_ G in H by Th55;
then 1_ G in the carrier of H by STRUCT_0:def 5;
then x = 1_ G by A1, TARSKI:def 1;
hence H = (1). G by A1, Def7; :: thesis: verum