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: Cl X c= Y by A1, PSCOMP_1:32;
A3: upper_bound X = upper_bound (Cl X) by TOPREAL6:78;
upper_bound (Cl X) in Cl X by RCOMP_1:30;
hence upper_bound X in Y by A2, A3; :: thesis: verum