let T be non empty strict TopSpace; :: thesis: for A, B being Subset of T st A is a_neighborhood of B holds
Top2NTop A is a_neighborhood of Top2NTop B
let A, B be Subset of T; :: thesis: ( A is a_neighborhood of B implies Top2NTop A is a_neighborhood of Top2NTop B )
reconsider NT = Top2NTop T as NTopSpace ;
reconsider TA = Top2NTop A, TB = Top2NTop B as Subset of NT ;
assume A is a_neighborhood of B ; :: thesis: Top2NTop A is a_neighborhood of Top2NTop B
then A1: B c= Int A by CONNSP_2:def 2;
now :: thesis: for x being Element of NT st x in TB holds
TA in U_FMT x
let x be Element of NT; :: thesis: ( x in TB implies TA in U_FMT x )
assume x in TB ; :: thesis: TA in U_FMT x
then x in Int A by A1;
then x in Int TA by Lm30;
then ex x9 being Point of NT st
( x = x9 & x9 is_interior_point_of TA ) ;
hence TA in U_FMT x by FINTOPO7:def 5; :: thesis: verum
end;
hence Top2NTop A is a_neighborhood of Top2NTop B by FINTOPO7:def 6; :: thesis: verum