let A, B be non empty Interval; :: thesis: ( sup A = inf B & ( sup A in A or inf B in B ) implies A \/ B is Interval )
assume A1: ( sup A = inf B & ( sup A in A or inf B in B ) ) ; :: thesis: A \/ B is Interval
then ( A is right_end or B is left_end ) by XXREAL_2:def 5, XXREAL_2:def 6;
hence A \/ B is Interval by A1, XXREAL_2:94, XXREAL_2:95; :: thesis: verum