theorem :: FINTOPO8:48

for T being non empty strict TopSpace
for A, B being Subset of T st A is a_neighborhood of B holds
Top2NTop A is a_neighborhood of Top2NTop B by Lm31;