theorem :: ANPROJ10:39

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