for NT being NTopSpace
for A being Subset of NT holds A is Subset of (NTop2Top NT) by FINTOPO7:def 16;