theorem Th31: :: EUCLIDLP:31

for n being Nat
for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
ex a being Real st y2 - y1 = a * (x2 - x1)