let G be Group; :: thesis: for a being Element of G
for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
( a * H1 c= a * H2 & H1 * a c= H2 * a )
let a be Element of G; :: thesis: for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
( a * H1 c= a * H2 & H1 * a c= H2 * a )
let H1, H2 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 implies ( a * H1 c= a * H2 & H1 * a c= H2 * a ) )
assume H1 is Subgroup of H2 ; :: thesis: ( a * H1 c= a * H2 & H1 * a c= H2 * a )
then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
hence ( a * H1 c= a * H2 & H1 * a c= H2 * a ) by Th4; :: thesis: verum