theorem :: RLAFFIN1:83

for r, s being Real
for V being RealLinearSpace
for v1, v2, w being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )