:: deftheorem Def9 defines closed FINTOPO8:def 9 :
for NTX being NTopSpace
for A being Subset of NTX holds
( A is closed iff ([#] NTX) \ A is open Subset of NTX );