:: deftheorem Def5 defines sum SEMI_AF1:def 5 :
for SAS being Semi_Affine_Space
for a, b, o, b₅ being Element of SAS holds
( b₅ = sum (a,b,o) iff congr o,a,b,b₅ );