for n being Nat
for x1, x2, x3 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L & x3 in L & x1 <> x2 holds
ex a being Real st x3 - x1 = a * (x2 - x1)