theorem Th2: :: JORDAN_A:2
for A being compact Subset of REAL
for B being non empty Subset of REAL st B c= A holds
lower_bound B in A