let V be RealLinearSpace; for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q holds
cross-ratio (R,S,Q,P) = 1 / (cross-ratio (P,Q,R,S))
let P, Q, R, S be Element of V; ( P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies cross-ratio (R,S,Q,P) = 1 / (cross-ratio (P,Q,R,S)) )
assume that
A1:
P,Q,R,S are_collinear
and
A2:
P <> R
and
A3:
P <> S
and
A4:
R <> Q
and
A5:
S <> Q
; cross-ratio (R,S,Q,P) = 1 / (cross-ratio (P,Q,R,S))
A6:
cross-ratio (P,Q,S,R) = 1 / (cross-ratio (P,Q,R,S))
by XCMPLX_1:57;
( P,Q,S,R are_collinear & P <> R & P <> S & R <> Q & S <> Q )
by A1, A2, A3, A4, A5;
hence
cross-ratio (R,S,Q,P) = 1 / (cross-ratio (P,Q,R,S))
by A6, Th34bis; verum