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 Lm4; :: thesis: verum