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 that
A1: sup A = inf B and
A2: ( sup A in A or inf B in B ) ; :: thesis: A \/ B is Interval
( A is with_max or B is with_min ) by A2, XXREAL_2:def 5, XXREAL_2:def 6;
hence A \/ B is Interval by A1, XXREAL_2:94, XXREAL_2:95; :: thesis: verum