let X be non empty real-membered bounded_below set ; :: thesis: for Y being closed Subset of REAL st X c= Y holds
inf X in Y
let Y be closed Subset of REAL ; :: thesis: ( X c= Y implies inf X in Y )
assume A1: X c= Y ; :: thesis: inf X in Y
reconsider X = X as non empty bounded_below Subset of REAL by MEMBERED:3;
A2: ( lower_bound X = lower_bound (Cl X) & lower_bound (Cl X) in Cl X ) by RCOMP_1:31, TOPREAL6:77;
Cl X c= Y by A1, PSCOMP_1:32;
hence inf X in Y by A2; :: thesis: verum