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 Th22
.= X by Th21 ;
hence ( X is bounded_below iff q3 ++ X is bounded_below ) by Lm5; :: thesis: verum