let X be Subset of REAL; :: thesis: for p being Real st X is bounded_below holds
p ++ X is bounded_below
let p be Real; :: thesis: ( X is bounded_below implies p ++ X is bounded_below )
given s being Real such that A1: s is LowerBound of X ; :: according to XXREAL_2:def 9 :: thesis: p ++ X is bounded_below
take p + s ; :: according to XXREAL_2:def 9 :: thesis: p + s is LowerBound of p ++ X
let t be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not t in p ++ X or p + s <= t )
assume t in p ++ X ; :: thesis: p + s <= t
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 2;
hence p + s <= t by A2, XREAL_1:6; :: thesis: verum