theorem Th28:
for
V being
RealLinearSpace for
P,
Q,
R being
Element of
V st
P,
Q,
R are_collinear &
P <> R &
Q <> R &
P <> Q holds
ex
r being non
zero non
unit Real st
(
r = affine-ratio (
P,
Q,
R) &
affine-ratio (
P,
R,
Q)
= op1 r &
affine-ratio (
Q,
P,
R)
= op1 (op2 (op1 r)) &
affine-ratio (
Q,
R,
P)
= op2 (op1 r) &
affine-ratio (
R,
P,
Q)
= op1 (op2 r) &
affine-ratio (
R,
Q,
P)
= op2 r )