theorem :: ANPROJ10:21

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;