for NT being NTopSpace
for A, B being Subset of NT st A is a_neighborhood of B holds
NTop2Top A is a_neighborhood of NTop2Top B