let SAS be Semi_Affine_Space; for a, o being Element of SAS holds congr a,o,o, opposite (a,o)
let a, o be Element of SAS; 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; verum