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