for x1, x2, x3, x4 being Element of (TOP-REAL 1) st x2 <> x3 & x3 <> x1 & x2 <> x4 & x1 <> x4 holds
ex a, b, c, d being Real st
( x1 = <*a*> & x2 = <*b*> & x3 = <*c*> & x4 = <*d*> & cross-ratio-tuple <*x1,x2,x3,x4*> = ((c - a) / (c - b)) * ((d - b) / (d - a)) )