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 sum a,x,o = sum a,y,o ; :: thesis: x = y
then ( sum a,x,o = sum a,y,o & congr o,a,x, sum a,x,o & congr o,a,y, sum a,y,o ) by Def5;
then ( congr a,o, sum a,x,o,x & congr a,o, sum a,x,o,y ) by Th89;
hence x = y by Th81; :: thesis: verum