let SAS be Semi_Affine_Space; :: thesis: for a, o being Element of SAS st sum a,a,o = o holds
a = o
let a, o be Element of SAS; :: thesis: ( sum a,a,o = o implies a = o )
assume sum a,a,o = o ; :: thesis: a = o
then congr o,a,a,o by Def5;
hence a = o by Th75; :: thesis: verum