theorem Th18: :: ANPROJ10:31

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