let A be compact Subset of REAL; :: thesis: for B being non empty Subset of REAL st B c= A holds
lower_bound B in A
let B be non empty Subset of REAL; :: thesis: ( B c= A implies lower_bound B in A )
assume A1: B c= A ; :: thesis: lower_bound B in A
A2: A is real-bounded by RCOMP_1:10;
then A3: B is bounded_below by A1, XXREAL_2:44;
A4: Cl B c= A by A1, MEASURE6:57;
Cl B is bounded_below by A1, A2, MEASURE6:57, XXREAL_2:44;
then lower_bound (Cl B) in Cl B by RCOMP_1:13;
then lower_bound (Cl B) in A by A4;
hence lower_bound B in A by A3, TOPREAL6:68; :: thesis: verum