:: deftheorem defines NTop2Top FINTOPO8:def 16 :
for NT being NTopSpace
for S being Subset of NT holds NTop2Top S = S;