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