theorem :: FINTOPO8:25
for NT being NTopSpace
for A being Subset of NT holds
( A is closed iff Cl A = A ) by Lm20, Lm22;