let V be RealLinearSpace; for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple (pi_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) )
let P, Q, R, S be Element of V; for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple (pi_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) )
let x be Tuple of 4, the carrier of V; ( x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear implies ( cross-ratio-tuple (pi_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) ) )
assume that
A1:
x = <*P,Q,R,S*>
and
A2:
P,Q,R,S are_mutually_distinct
and
A3:
P,Q,R,S are_collinear
; ( cross-ratio-tuple (pi_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) )
A4:
( P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q )
by A2, ZFMISC_1:def 6;
cross-ratio (P,Q,R,S) <> 0
by A3, A4, Th31;
then reconsider cr = cross-ratio-tuple x as non zero Complex by A1, Th36;
( pi_1243 x = <*P,Q,S,R*> & P,Q,S,R are_collinear & P,Q,S,R are_mutually_distinct )
by A4, A1, A3, ZFMISC_1:def 6;
then A5: cross-ratio-tuple (pi_1324 (pi_1243 x)) =
1 - (cross-ratio-tuple (pi_1243 x))
by Th41
.=
1 - (1 / cr)
by A1, A3, A4, Th40
.=
(cr / cr) - (1 / cr)
by XCMPLX_1:60
.=
(cr - 1) / cr
;
hence
cross-ratio-tuple (pi_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x)
; ( cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) )
( pi_1423 x = <*P,S,Q,R*> & P,S,Q,R are_collinear )
by A1, A3;
then
( cross-ratio-tuple (pi_3412 (pi_1423 x)) = cross-ratio-tuple (pi_1423 x) & cross-ratio-tuple (pi_2143 (pi_1423 x)) = cross-ratio-tuple (pi_1423 x) & cross-ratio-tuple (pi_4321 (pi_1423 x)) = cross-ratio-tuple (pi_1423 x) )
by A4, Th37, Th38;
hence
( cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) )
by A5; verum