theorem Th1: :: MEASUR12:1

for A, B being non empty Interval st A is open_interval & B is open_interval & A \/ B is Interval holds
( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )