let G be addGroup; :: 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 DefA5;
hence ( a + H1 c= a + H2 & H1 + a c= H2 + a ) by Th4; :: thesis: verum