theorem :: XXREAL_2:87

for A being ext-real-membered set st ( for r being ExtReal st inf A < r & r < sup A holds
r in A ) holds
A is interval