:: deftheorem defines NTop2Top FINTOPO8:def 18 :
for TX, TY being NTopSpace
for f being Function of TX,TY holds NTop2Top f = f;