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