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