let A, B be open_interval Subset of REAL; :: thesis: ( A meets B implies A \/ B is open_interval Subset of REAL )
assume A meets B ; :: thesis: A \/ B is open_interval Subset of REAL
then ( A <> {} & B <> {} & A \/ B is interval ) by XBOOLE_1:65, XXREAL_2:89;
hence A \/ B is open_interval Subset of REAL by Th1; :: thesis: verum