let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum