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 bounded by RCOMP_1:28;
then A3: B is bounded_below by A1, XXREAL_2:44;
A4: Cl B c= A by A1, MEASURE6:93;
Cl B is bounded_below by A1, A2, MEASURE6:93, XXREAL_2:44;
then lower_bound (Cl B) in Cl B by RCOMP_1:31;
then lower_bound (Cl B) in A by A4;
hence lower_bound B in A by A3, TOPREAL6:77; :: thesis: verum