let T be non empty strict TopSpace; :: thesis: for A being Subset of T
for x being Point of T st A is a_neighborhood of x holds
Top2NTop A is a_neighborhood of Top2NTop x
let A be Subset of T; :: thesis: for x being Point of T st A is a_neighborhood of x holds
Top2NTop A is a_neighborhood of Top2NTop x
let x be Point of T; :: thesis: ( A is a_neighborhood of x implies Top2NTop A is a_neighborhood of Top2NTop x )
reconsider NT = Top2NTop T as NTopSpace ;
reconsider NA = Top2NTop A as Subset of NT ;
reconsider Nx = Top2NTop x as Point of NT ;
assume A is a_neighborhood of x ; :: thesis: Top2NTop A is a_neighborhood of Top2NTop x
then x in Int A by CONNSP_2:def 1;
then Nx in Int NA by Lm30;
then ex y being Point of NT st
( Nx = y & y is_interior_point_of NA ) ;
hence Top2NTop A is a_neighborhood of Top2NTop x ; :: thesis: verum