for G being addGroup
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) + a = (H1 + a) /\ (H2 + a)