theorem :: URYSOHN2:26

for A being non empty Subset of ExtREAL
for a, b being R_eal st A c= [.a,b.] holds
( a <= inf A & sup A <= b )