theorem :: FINTOPO8:21

for NT being NTopSpace
for A being closed Subset of NT holds A is closed Subset of (NTop2Top NT) by Lm29;