let V be RealLinearSpace; :: thesis: for P, Q, R, S, P9, Q9, R9, S9 being Element of V st P,Q,R,S are_collinear & P9,Q9,R9,S9 are_collinear & S <> P & S <> Q & S9 <> P9 & S9 <> Q9 holds
( cross-ratio (P,Q,R,S) = cross-ratio (P9,Q9,R9,S9) iff (affine-ratio (R,P,Q)) * (affine-ratio (S9,P9,Q9)) = (affine-ratio (R9,P9,Q9)) * (affine-ratio (S,P,Q)) )
let P, Q, R, S, P9, Q9, R9, S9 be Element of V; :: thesis: ( P,Q,R,S are_collinear & P9,Q9,R9,S9 are_collinear & S <> P & S <> Q & S9 <> P9 & S9 <> Q9 implies ( cross-ratio (P,Q,R,S) = cross-ratio (P9,Q9,R9,S9) iff (affine-ratio (R,P,Q)) * (affine-ratio (S9,P9,Q9)) = (affine-ratio (R9,P9,Q9)) * (affine-ratio (S,P,Q)) ) )
assume that
A1: P,Q,R,S are_collinear and
A2: P9,Q9,R9,S9 are_collinear and
A3: S <> P and
A4: S <> Q and
A5: S9 <> P9 and
A6: S9 <> Q9 ; :: thesis: ( cross-ratio (P,Q,R,S) = cross-ratio (P9,Q9,R9,S9) iff (affine-ratio (R,P,Q)) * (affine-ratio (S9,P9,Q9)) = (affine-ratio (R9,P9,Q9)) * (affine-ratio (S,P,Q)) )
set r = affine-ratio (R,P,Q);
set s = affine-ratio (S,P,Q);
set r9 = affine-ratio (R9,P9,Q9);
set s9 = affine-ratio (S9,P9,Q9);
( S,P,Q are_collinear & S9,P9,Q9 are_collinear ) by A1, A2;
then ( affine-ratio (S,P,Q) <> 0 & affine-ratio (S9,P9,Q9) <> 0 ) by A3, A4, A5, A6, Th06;
hence ( cross-ratio (P,Q,R,S) = cross-ratio (P9,Q9,R9,S9) iff (affine-ratio (R,P,Q)) * (affine-ratio (S9,P9,Q9)) = (affine-ratio (R9,P9,Q9)) * (affine-ratio (S,P,Q)) ) by XCMPLX_1:94, XCMPLX_1:95; :: thesis: verum