let X be Subset of REAL; :: thesis: for s being Real st X is bounded_above holds
s ++ X is bounded_above
let p be Real; :: thesis: ( X is bounded_above implies p ++ X is bounded_above )
given s being Real such that A1: s is UpperBound of X ; :: according to XXREAL_2:def 10 :: thesis: p ++ X is bounded_above
take p + s ; :: according to XXREAL_2:def 10 :: thesis: p + s is UpperBound of p ++ X
let t be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not t in p ++ X or t <= p + s )
assume t in p ++ X ; :: thesis: t <= p + s
then t in { (p + r3) where r3 is Real : r3 in X } by Lm5;
then consider r3 being Real such that
A2: t = p + r3 and
A3: r3 in X ;
r3 <= s by A1, A3, XXREAL_2:def 1;
hence t <= p + s by A2, XREAL_1:6; :: thesis: verum