theorem Th38: :: ANPROJ10:69

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_collinear & P <> R & P <> S & Q <> R & Q <> S holds
( cross-ratio-tuple x = cross-ratio-tuple (pi_2143 x) & cross-ratio-tuple x = cross-ratio-tuple (pi_4321 x) )