theorem :: XXREAL_2:85

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