theorem :: EUCLID12:41

for L1, L2 being Element of line_of_REAL 2 st L1 is being_line & L2 is being_line & L1 misses L2 holds
L1 // L2 by Th31, EUCLIDLP:113;