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