theorem Th31: :: ANPROJ10:52

for V being RealLinearSpace
for P, Q, R, S being Element of V st P,Q,R,S are_collinear & R <> Q & S <> Q & S <> P holds
( R = P iff cross-ratio (P,Q,R,S) = 0 )