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 Th69;
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 Th69;
hence a,b // opposite (a,o), opposite (b,o) by A1, Th73; :: thesis: verum