theorem :: ANPROJ10:76

for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple (pi_1432 x) = (cross-ratio-tuple x) / ((cross-ratio-tuple x) - 1) & cross-ratio-tuple (pi_2341 x) = (cross-ratio-tuple x) / ((cross-ratio-tuple x) - 1) & cross-ratio-tuple (pi_3214 x) = (cross-ratio-tuple x) / ((cross-ratio-tuple x) - 1) & cross-ratio-tuple (pi_4123 x) = (cross-ratio-tuple x) / ((cross-ratio-tuple x) - 1) )