let X be Subset of REAL ; :: thesis: ( X is closed iff - X is closed )
- (- X) = X ;
hence ( X is closed iff - X is closed ) by Lm3; :: thesis: verum