for NT being NTopSpace
for A being Subset of NT
for a being Point of NT st A is a_neighborhood of a holds
NTop2Top A is a_neighborhood of NTop2Top a