:: deftheorem defines NTop2Top FINTOPO8:def 14 :
for NT being NTopSpace
for x being Point of NT holds NTop2Top x = x;