for G being addGroup
for a being Element of G
for A, B being Subset of G st A c= B holds
( a + A c= a + B & A + a c= B + a ) by Th4;