theorem :: ANPROJ10:12

for V being RealLinearSpace
for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
A - B = (affine-ratio (A,B,C)) * (A - C)