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 (P,Q,R,S) = cross-ratio (S,R,Q,P)
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 (P,Q,R,S) = cross-ratio (S,R,Q,P) )
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 (P,Q,R,S) = cross-ratio (S,R,Q,P)
R,S,P,Q are_collinear by A1;
then cross-ratio (R,S,P,Q) = cross-ratio (S,R,Q,P) by A2, A3, A4, A5, Th34;
hence cross-ratio (P,Q,R,S) = cross-ratio (S,R,Q,P) by A1, A3, A4, A5, Th33; :: thesis: verum