let V be RealLinearSpace; for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct holds
cross-ratio (S,Q,R,P) = 1 - (cross-ratio (P,Q,R,S))
let P, Q, R, S be Element of V; ( P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies cross-ratio (S,Q,R,P) = 1 - (cross-ratio (P,Q,R,S)) )
assume that
A1:
P,Q,R,S are_collinear
and
A2:
P,Q,R,S are_mutually_distinct
; cross-ratio (S,Q,R,P) = 1 - (cross-ratio (P,Q,R,S))
A3:
( P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q )
by A2, ZFMISC_1:def 6;
P,R,Q,S are_collinear
by A1;
then
cross-ratio (S,Q,R,P) = cross-ratio (P,R,Q,S)
by A3, Th34bis;
hence
cross-ratio (S,Q,R,P) = 1 - (cross-ratio (P,Q,R,S))
by A1, A2, Th35; verum