let G be Group; :: thesis: for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
for a being Element of G holds H1 |^ a is Subgroup of H2 |^ a
let H1, H2 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 implies for a being Element of G holds H1 |^ a is Subgroup of H2 |^ a )
assume A1: H1 is Subgroup of H2 ; :: thesis: for a being Element of G holds H1 |^ a is Subgroup of H2 |^ a
let a be Element of G; :: thesis: H1 |^ a is Subgroup of H2 |^ a
for h being Element of G st h in H1 |^ a holds
h in H2 |^ a

proof

let h be Element of G; :: thesis: ( h in H1 |^ a implies h in H2 |^ a )
assume h in H1 |^ a ; :: thesis: h in H2 |^ a
then consider g being Element of G such that
B1: ( h = g |^ a & g in H1 ) by GROUP_3:58;
g in H2 by A1, B1, GROUP_2:40;
hence h in H2 |^ a by B1, GROUP_3:58; :: thesis: verum

end;

hence H1 |^ a is Subgroup of H2 |^ a by GROUP_2:58; :: thesis: verum