for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being Real holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )