let G be addGroup; :: thesis: for a being Element of G
for H being strict Subgroup of G st H * a = (0). G holds
H = (0). G
let a be Element of G; :: thesis: for H being strict Subgroup of G st H * a = (0). G holds
H = (0). G
let H be strict Subgroup of G; :: thesis: ( H * a = (0). G implies H = (0). G )
assume A1: H * a = (0). G ; :: thesis: H = (0). G
then reconsider H = H as finite Subgroup of G by Th65;
card ((0). G) = 1 by Th69;
then card H = 1 by A1, Th64;
hence H = (0). G by Th70; :: thesis: verum