theorem Th34bis: :: ANPROJ10:58
for V being RealLinearSpace
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)