for X being Subset of REAL holds
( X is closed iff X = Cl X )