let L1, L2 be Element of line_of_REAL 2; :: thesis: ( L1 _|_ L2 implies ex x being Element of REAL 2 st L1 /\ L2 = {x} )
assume A1: L1 _|_ L2 ; :: thesis: ex x being Element of REAL 2 st L1 /\ L2 = {x}
then A2: ( L1 is being_line & L2 is being_line ) by EUCLIDLP:67;
A3: ( L1 <> L2 & L1 meets L2 ) by A1, EUCLIDLP:75, Th31, EUCLIDLP:109;
for x being Element of REAL 2 holds
( not L1 = {x} & not L2 = {x} ) by A2, Th7;
hence ex x being Element of REAL 2 st L1 /\ L2 = {x} by A3, Th32; :: thesis: verum