theorem Th9: :: JORDAN6:9

for r being Real
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds
P is closed