let x, y be Real; :: thesis: for x1, y1 being Point of RNS_Real st x = x1 & y = y1 holds
x - y = x1 - y1
let x1, y1 be Point of RNS_Real; :: thesis: ( x = x1 & y = y1 implies x - y = x1 - y1 )
assume AS: ( x = x1 & y = y1 ) ; :: thesis: x - y = x1 - y1
then P1: - y = - y1 by RNS3;
x - y = x + (- y) ;
hence x - y = x1 - y1 by AS, BINOP_2:def 9, P1; :: thesis: verum