theorem Th16: :: EUCLID12:20

for L1, L2 being Element of line_of_REAL 2 holds
( L1 // L2 or 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} ) )