let NT be NTopSpace; :: thesis: for A being Subset of NT
for x being Point of NT st A is a_neighborhood of x holds
Int A is open a_neighborhood of x
let A be Subset of NT; :: thesis: for x being Point of NT st A is a_neighborhood of x holds
Int A is open a_neighborhood of x
let x be Point of NT; :: thesis: ( A is a_neighborhood of x implies Int A is open a_neighborhood of x )
assume A is a_neighborhood of x ; :: thesis: Int A is open a_neighborhood of x
then x is_interior_point_of A ;
then x in Int A ;
then x in Int (Int A) by Th12;
then ex y being Point of NT st
( x = y & y is_interior_point_of Int A ) ;
then reconsider IA = Int A as a_neighborhood of x ;
IA is open a_neighborhood of x ;
hence Int A is open a_neighborhood of x ; :: thesis: verum