theorem Th65: :: EUCLIDLP:65

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