theorem
for
V being
RealLinearSpace for
P,
Q,
R being
Element of
V for
r being
Real st
P,
Q,
R are_collinear &
P <> R &
Q <> R &
P <> Q &
r = affine-ratio (
P,
Q,
R) holds
(
affine-ratio (
P,
R,
Q)
= 1
/ r &
affine-ratio (
Q,
P,
R)
= r / (r - 1) &
affine-ratio (
Q,
R,
P)
= (r - 1) / r &
affine-ratio (
R,
P,
Q)
= 1
/ (1 - r) &
affine-ratio (
R,
Q,
P)
= 1
- r )
by Th09, Th10, Th11, Th12, Th13;