let X be non empty real-membered bounded_below set ; :: thesis: for Y being closed Subset of REAL st X c= Y holds
lower_bound X in Y
let Y be closed Subset of REAL; :: thesis: ( X c= Y implies lower_bound X in Y )
assume A1: X c= Y ; :: thesis: lower_bound 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:13, TOPREAL6:68;
Cl X c= Y by A1, MEASURE6:57;
hence lower_bound X in Y by A2; :: thesis: verum