let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: p,q // sum p,r,o, sum q,r,o
( congr o,p,r, sum p,r,o & congr o,q,r, sum q,r,o ) by Def5;
then ( congr p,o, sum p,r,o,r & congr o,q,r, sum q,r,o ) by Th89;
hence p,q // sum p,r,o, sum q,r,o by Th76, Th90; :: thesis: verum