let G be Group; :: thesis: for a being Element of G
for H being strict Subgroup of G st H |^ a = (1). G holds
H = (1). G
let a be Element of G; :: thesis: for H being strict Subgroup of G st H |^ a = (1). G holds
H = (1). G
let H be strict Subgroup of G; :: thesis: ( H |^ a = (1). G implies H = (1). G )
assume A1: H |^ a = (1). G ; :: thesis: H = (1). G
then reconsider H = H as finite Subgroup of G by Th65;
card ((1). G) = 1 by GROUP_2:69;
then card H = 1 by A1, Th64;
hence H = (1). G by GROUP_2:70; :: thesis: verum