theorem
for
V being
RealLinearSpace 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)) )