let V be RealLinearSpace; :: thesis: 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 (S,R,P,Q) = 1 / (cross-ratio (P,Q,R,S))
let P, Q, R, S be Element of V; :: thesis: ( P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies cross-ratio (S,R,P,Q) = 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 ; :: thesis: cross-ratio (S,R,P,Q) = 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;
( S,R,P,Q are_collinear & P <> R & P <> S & R <> Q & S <> Q ) by A1, A2, A3, A4, A5;
hence cross-ratio (S,R,P,Q) = 1 / (cross-ratio (P,Q,R,S)) by A6, Th33; :: thesis: verum