let SAS be Semi_Affine_Space; :: thesis: for o, b, a being Element of SAS holds o, diff b,a,o // a,b
let o, b, a be Element of SAS; :: thesis: o, diff b,a,o // a,b
( diff b,a,o = sum b,(opposite a,o),o & congr o,b, opposite a,o, sum b,(opposite a,o),o ) by Def5;
then ( congr o, opposite a,o,b, diff b,a,o & congr a,o,o, opposite a,o ) by Th89, Th106;
then ( congr o, opposite a,o,b, diff b,a,o & congr o, opposite a,o,a,o ) by Th89;
then congr a,o,b, diff b,a,o by Th85;
then congr o, diff b,a,o,a,b by Th89;
hence o, diff b,a,o // a,b by Th76; :: thesis: verum