for H being non empty addMagma
for P, Q being Subset of H holds the addF of H .: [:P,Q:] = P + Q