for n being Nat
for A being Subset of (TOP-REAL n)
for a being Real st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
( A ` is open & A is closed )