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 Th78;
card ((1). G) = 1 by GROUP_2:81;
then card H = 1 by A1, Th77;
hence H = (1). G by GROUP_2:82; :: thesis: verum