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