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

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