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
congr a,o,o, opposite a,o by Th106;
then A1: congr o, opposite a,o,a,o by Th89;
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 by Th89;
then congr a,o,b, diff b,a,o by A1, Th85;
then congr o, diff b,a,o,a,b by Th89;
hence o, diff b,a,o // a,b by Th76; :: thesis: verum