theorem :: ANPROJ10:25

for x, y being Element of (TOP-REAL 1)
for p, q being Tuple of 1, REAL st p = x & q = y holds
x - y = p - q ;