let G be Group; :: thesis: for a being Element of G
for H being strict Subgroup of G st H |^ a = G holds
H = G
let a be Element of G; :: thesis: for H being strict Subgroup of G st H |^ a = G holds
H = G
let H be strict Subgroup of G; :: thesis: ( H |^ a = G implies H = G )
assume A1: H |^ a = G ; :: thesis: H = G

now

let g be Element of G; :: thesis: g in H
assume A2: not g in H ; :: thesis: contradiction

now

assume g |^ a in H |^ a ; :: thesis: contradiction
then ex h being Element of G st
( g |^ a = h |^ a & h in H ) by Th70;
hence contradiction by A2, Th21; :: thesis: verum

end;

hence contradiction by A1, STRUCT_0:def 5; :: thesis: verum

end;

hence H = G by A1, GROUP_2:71; :: thesis: verum