for G being addGroup
for H1, H2 being Subgroup of G holds (0). H1 = (0). H2