theorem Th35: :: ANPROJ10:63

for V being RealLinearSpace
for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct holds
cross-ratio (P,R,Q,S) = 1 - (cross-ratio (P,Q,R,S))