let SAS be Semi_Affine_Space; :: thesis: for a, b, o being Element of SAS holds a,b // opposite a,o, opposite b,o
let a, b, o be Element of SAS; :: thesis: a,b // opposite a,o, opposite b,o
sum b,(opposite b,o),o = o by Def6;
then congr o,b, opposite b,o,o by Def5;
then A1: congr b,o,o, opposite b,o by Th89;
sum a,(opposite a,o),o = o by Def6;
then congr o,a, opposite a,o,o by Def5;
then congr a,o,o, opposite a,o by Th89;
hence a,b // opposite a,o, opposite b,o by A1, Th93; :: thesis: verum