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 a,(opposite a,o),o = o & sum b,(opposite b,o),o = o ) by Def6;
then ( congr o,a, opposite a,o,o & congr o,b, opposite b,o,o ) by Def5;
then ( congr a,o,o, opposite a,o & congr b,o,o, opposite b,o ) by Th89;
hence a,b // opposite a,o, opposite b,o by Th93; :: thesis: verum