theorem :: ANPROJ10:46

for x, y being Element of (TOP-REAL 1)
for a, b being Real st x = <*a*> & y = <*b*> holds
x - y = <*(a - b)*> by RVSUM_1:29;