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