theorem :: EUCLID12:40

for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 holds
L1 meets L2 by Th31, EUCLIDLP:109;