theorem :: COUSIN2:14

for r being Real
for s being ExtReal
for A being Subset of REAL st A c= ].s,r.[ holds
A is bounded_above