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 Th69; :: thesis: verum