theorem :: COUSIN2:13

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