theorem Th66: :: EUCLIDLP:66

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 // L2 holds
( L1 is being_line & L2 is being_line )