let SAS be Semi_Affine_Space; :: thesis: for a, b, o being Element of SAS holds o, diff (b,a,o) // a,b
let a, b, o be Element of SAS; :: thesis: o, diff (b,a,o) // a,b
congr a,o,o, opposite (a,o) by Th81;
then A1: congr o, opposite (a,o),a,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) by Th69;
then congr a,o,b, diff (b,a,o) by A1, Th65;
then congr o, diff (b,a,o),a,b by Th69;
hence o, diff (b,a,o) // a,b by Th57; :: thesis: verum