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 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; :: thesis: verum