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