theorem :: XXREAL_2:90

for A, B being ext-real-membered set st A is interval & B is left_end & B is interval & sup A = inf B holds
A \/ B is interval