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