theorem Th39: :: ANPROJ10:70

for V being RealLinearSpace
for x being Tuple of 4, the carrier of V holds cross-ratio-tuple (pi_1243 x) = 1 / (cross-ratio-tuple x)