theorem Th1: :: INTEGRA1:3

for A being non empty closed_interval Subset of REAL holds
( A is bounded_below & A is bounded_above )