let x1, x2, x3, x4 be Element of (TOP-REAL 1); :: thesis: ( x2 <> x3 & x3 <> x1 & x2 <> x4 & x1 <> x4 implies 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)) ) )
assume that
A1: x2 <> x3 and
A2: x3 <> x1 and
A3: x2 <> x4 and
A4: x1 <> x4 ; :: thesis: 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)) )
reconsider x = <*x1,x2,x3,x4*> as Tuple of 4, the carrier of (TOP-REAL 1) ;
consider P, Q, R, S being Element of (TOP-REAL 1) such that
A5: ( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & cross-ratio-tuple x = cross-ratio (P,Q,R,S) ) by Def03;
consider a1, b1, c1 being Real such that
A7: ( x3 = <*a1*> & x1 = <*b1*> & x2 = <*c1*> & affine-ratio (x3,x1,x2) = (b1 - a1) / (c1 - a1) ) by A1, A2, Th26;
consider a2, b2, c2 being Real such that
A8: ( x4 = <*a2*> & x1 = <*b2*> & x2 = <*c2*> & affine-ratio (x4,x1,x2) = (b2 - a2) / (c2 - a2) ) by A3, A4, Th26;
take b1 ; :: thesis: ex b, c, d being Real st
( x1 = <*b1*> & x2 = <*b*> & x3 = <*c*> & x4 = <*d*> & cross-ratio-tuple <*x1,x2,x3,x4*> = ((c - b1) / (c - b)) * ((d - b) / (d - b1)) )
take c1 ; :: thesis: ex c, d being Real st
( x1 = <*b1*> & x2 = <*c1*> & x3 = <*c*> & x4 = <*d*> & cross-ratio-tuple <*x1,x2,x3,x4*> = ((c - b1) / (c - c1)) * ((d - c1) / (d - b1)) )
take a1 ; :: thesis: ex d being Real st
( x1 = <*b1*> & x2 = <*c1*> & x3 = <*a1*> & x4 = <*d*> & cross-ratio-tuple <*x1,x2,x3,x4*> = ((a1 - b1) / (a1 - c1)) * ((d - c1) / (d - b1)) )
take a2 ; :: thesis: ( x1 = <*b1*> & x2 = <*c1*> & x3 = <*a1*> & x4 = <*a2*> & cross-ratio-tuple <*x1,x2,x3,x4*> = ((a1 - b1) / (a1 - c1)) * ((a2 - c1) / (a2 - b1)) )
( b1 = b2 & c1 = c2 ) by A7, A8, FINSEQ_1:76;
hence ( x1 = <*b1*> & x2 = <*c1*> & x3 = <*a1*> & x4 = <*a2*> & cross-ratio-tuple <*x1,x2,x3,x4*> = ((a1 - b1) / (a1 - c1)) * ((a2 - c1) / (a2 - b1)) ) by A7, A8, Lm03, A5; :: thesis: verum