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