let NT be NTopSpace; :: thesis: for A, B being Subset of NT st A is a_neighborhood of B holds
NTop2Top A is a_neighborhood of NTop2Top B
let A, B be Subset of NT; :: thesis: ( A is a_neighborhood of B implies NTop2Top A is a_neighborhood of NTop2Top B )
assume A1: A is a_neighborhood of B ; :: thesis: NTop2Top A is a_neighborhood of NTop2Top B
reconsider T = NTop2Top NT as TopSpace ;
reconsider TA = NTop2Top A, TB = NTop2Top B as Subset of T ;
per cases ( not B is empty or B is empty ) ;
suppose not B is empty ; :: thesis: NTop2Top A is a_neighborhood of NTop2Top B
then consider O being open Subset of NT such that
A2: B c= O and
A3: O c= A by A1, FINTOPO7:16;
reconsider O9 = O as open Subset of T by Lm9;
O9 c= Int TA by A3, TOPS_1:24;
then TB c= Int TA by A2;
hence NTop2Top A is a_neighborhood of NTop2Top B by CONNSP_2:def 2; :: thesis: verum
end;
suppose B is empty ; :: thesis: NTop2Top A is a_neighborhood of NTop2Top B
then TB c= Int TA ;
hence NTop2Top A is a_neighborhood of NTop2Top B by CONNSP_2:def 2; :: thesis: verum
end;
end;