theorem Th79: :: EUCLIDLP:79

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 holds
ex x being Element of REAL n st
( x in L1 & not x in L2 )