:: deftheorem defines Top2NTop FINTOPO8:def 10 :
for S, T being non empty TopSpace
for f being Function of S,T holds Top2NTop f = f;