theorem :: FINTOPO8:28

for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
( A is open iff B is closed ) by Lm6;