theorem Th32: :: EUCLID12:42

for L1, L2 being Element of line_of_REAL 2 st L1 <> L2 & L1 meets L2 & ( for x being Element of REAL 2 holds
( not L1 = {x} & not L2 = {x} ) ) holds
( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} )