theorem :: ANPROJ10:53

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