let A be compact Subset of REAL ; :: thesis: for B being non empty Subset of REAL st B c= A holds
inf B in A
let B be non empty Subset of REAL ; :: thesis: ( B c= A implies inf B in A )
assume A1: B c= A ; :: thesis: inf 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, PSCOMP_1:32;
Cl B is bounded_below by A1, A2, PSCOMP_1:32, XXREAL_2:44;
then inf (Cl B) in Cl B by RCOMP_1:31;
then inf (Cl B) in A by A4;
hence inf B in A by A3, TOPREAL6:77; :: thesis: verum