for SAS being Semi_Affine_Space
for a, o being Element of SAS st sum (a,a,o) = o holds
a = o