theorem Th37:
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 <> S &
Q <> R &
Q <> S holds
cross-ratio-tuple x = cross-ratio-tuple (pi_3412 x)