theorem :: EUCLIDLP:50

for n being Nat
for x being Element of REAL n
for L0, L1 being Element of line_of_REAL n st L0 misses L1 & x in L0 holds
not x in L1 by Th49;