let L1, L2 be Element of line_of_REAL 2; :: thesis: ( L1 _|_ L2 implies not L1 // L2 )
assume L1 _|_ L2 ; :: thesis: not L1 // L2
then ( L1 <> L2 & L1 meets L2 ) by EUCLIDLP:75, Th31, EUCLIDLP:109;
hence not L1 // L2 by EUCLIDLP:71; :: thesis: verum