let X be non empty real-membered bounded_above set ; :: thesis: for Y being closed Subset of REAL st X c= Y holds
upper_bound X in Y
let Y be closed Subset of REAL; :: thesis: ( X c= Y implies upper_bound X in Y )
assume A1: X c= Y ; :: thesis: upper_bound X in Y
reconsider X = X as non empty bounded_above Subset of REAL by MEMBERED:3;
A2: ( upper_bound X = upper_bound (Cl X) & upper_bound (Cl X) in Cl X ) by RCOMP_1:12, TOPREAL6:69;
Cl X c= Y by A1, MEASURE6:57;
hence upper_bound X in Y by A2; :: thesis: verum