for X being Subset of REAL
for q3 being Real holds
( X is closed iff q3 ++ X is closed )