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

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