for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (a + b) + H = a + (b + H) by Th32;