for T being RealLinearSpace st T = TOP-REAL 1 holds
for x, y, z being Element of T st z <> x & y <> x holds
ex a, b, c being Real st
( x = <*a*> & y = <*b*> & z = <*c*> & affine-ratio (x,y,z) = (b - a) / (c - a) )