theorem :: ANPROJ10:45

for x, y being Element of (TOP-REAL 1)
for a, b, r being Real st x = <*a*> & y = <*b*> holds
( x = r * y iff a = r * b )