let G be addGroup; :: 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 :: thesis: for g being Element of G holds g in H
let g be Element of G; :: thesis: g in H
assume A2: not g in H ; :: thesis: contradiction
now :: thesis: not g * a in H * a
assume g * a in H * a ; :: thesis: contradiction
then ex h being Element of G st
( g * a = h * a & h in H ) by Th58;
hence contradiction by A2, ThB16; :: thesis: verum
end;
hence contradiction by A1; :: thesis: verum
end;
hence H = G by A1, Th62; :: thesis: verum