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 & carr H1 = the carrier of H1 & the carrier of H2 = carr H2 & a * H1 = a * (carr H1) & a * H2 = a * (carr H2) & H1 * a = (carr H1) * a & H2 * a = (carr H2) * a ) by GROUP_2:def 5;
hence ( a * H1 c= a * H2 & H1 * a c= H2 * a ) by Th4; :: thesis: verum