theorem RNS4: :: DUALSP03:4

for x, y being Real
for x1, y1 being Point of RNS_Real st x = x1 & y = y1 holds
x - y = x1 - y1