let r1, r2 be Real; :: thesis: ( B - A = r1 * (C - A) & B - A = r2 * (C - A) implies r1 = r2 )
assume that
A12: B - A = r1 * (C - A) and
A13: B - A = r2 * (C - A) ; :: thesis: r1 = r2
( C - A <> 0. V & r1 * (C - A) = r2 * (C - A) ) by A12, A13, A1, RLVECT_1:21;
hence r1 = r2 by RLVECT_1:37; :: thesis: verum