let SAS be Semi_Affine_Space; :: thesis: for a, x, o, y being Element of SAS st sum a,x,o = sum a,y,o holds
x = y
let a, x, o, 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 Th89;
congr o,a,y, sum a,y,o by Def5;
then congr a,o, sum a,x,o,y by A1, Th89;
hence x = y by A2, Th81; :: thesis: verum