for G being addGroup
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 )