let SAS be Semi_Affine_Space; for p, q, r, o being Element of SAS holds p,q // sum (p,r,o), sum (q,r,o)
let p, q, r, o be Element of SAS; p,q // sum (p,r,o), sum (q,r,o)
congr o,p,r, sum (p,r,o)
by Def5;
then A1:
congr p,o, sum (p,r,o),r
by Th89;
congr o,q,r, sum (q,r,o)
by Def5;
hence
p,q // sum (p,r,o), sum (q,r,o)
by A1, Th76, Th90; verum