let X be Subset of REAL; :: thesis: for q3 being Real holds
( X is bounded_below iff q3 ++ X is bounded_below )
let q3 be Real; :: thesis: ( X is bounded_below iff q3 ++ X is bounded_below )
(- q3) ++ (q3 ++ X) = ((- q3) + q3) ++ X by MEMBER_1:147
.= X by MEMBER_1:146 ;
hence ( X is bounded_below iff q3 ++ X is bounded_below ) by Lm7; :: thesis: verum