:: deftheorem defines Top2NTop FINTOPO8:def 15 :
for T being non empty TopSpace
for x being Point of T holds Top2NTop x = x;