theorem Th40: :: EUCLIDLP:40

for n being Nat
for x0, x1, x2, x3, y0, y1, y2, y3 being Element of REAL n st x1 - x0,x3 - x2 are_lindependent2 & y0 in Line (x0,x1) & y1 in Line (x0,x1) & y0 <> y1 & y2 in Line (x2,x3) & y3 in Line (x2,x3) & y2 <> y3 holds
y1 - y0,y3 - y2 are_lindependent2