let x1, x2, x3, x4 be Element of (TOP-REAL 1); ( 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
; 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
; 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
; 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
; 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
; ( 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; verum