theorem :: XXREAL_2:86

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