let L1, L2 be Element of line_of_REAL 2; :: thesis: ( L1 <> L2 & L1 meets L2 & ( for x being Element of REAL 2 holds

( not L1 = {x} & not L2 = {x} ) ) implies ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

assume that

A1: L1 <> L2 and

A2: L1 meets L2 ; :: thesis: ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

not L1 // L2 by A1, A2, EUCLIDLP:71;

hence ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) ) by Th16; :: thesis: verum

( not L1 = {x} & not L2 = {x} ) ) implies ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

assume that

A1: L1 <> L2 and

A2: L1 meets L2 ; :: thesis: ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

not L1 // L2 by A1, A2, EUCLIDLP:71;

hence ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) ) by Th16; :: thesis: verum