for A, B being open_interval Subset of REAL st A meets B holds
A \/ B is open_interval Subset of REAL