let NT be NTopSpace; :: thesis: 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
let A be Subset of NT; :: thesis: for a being Point of NT st A is a_neighborhood of a holds
NTop2Top A is a_neighborhood of NTop2Top a
let a be Point of NT; :: thesis: ( A is a_neighborhood of a implies NTop2Top A is a_neighborhood of NTop2Top a )
reconsider T = NTop2Top NT as non empty TopSpace ;
reconsider TA = NTop2Top A as Subset of T ;
reconsider Tx = NTop2Top a as Point of T ;
assume A is a_neighborhood of a ; :: thesis: NTop2Top A is a_neighborhood of NTop2Top a
then a is_interior_point_of A ;
then a in Int A ;
then Tx in Int TA by Th34;
hence NTop2Top A is a_neighborhood of NTop2Top a by CONNSP_2:def 1; :: thesis: verum