let X be non empty TopSpace; :: thesis: for x being Point of X
for U1 being Subset of X st U1 is a_neighborhood of x holds
ex V being non empty Subset of X st
( V is a_neighborhood of x & V is open & V c= U1 )
let x be Point of X; :: thesis: for U1 being Subset of X st U1 is a_neighborhood of x holds
ex V being non empty Subset of X st
( V is a_neighborhood of x & V is open & V c= U1 )
let U1 be Subset of X; :: thesis: ( U1 is a_neighborhood of x implies ex V being non empty Subset of X st
( V is a_neighborhood of x & V is open & V c= U1 ) )
assume U1 is a_neighborhood of x ; :: thesis: ex V being non empty Subset of X st
( V is a_neighborhood of x & V is open & V c= U1 )
then x in Int U1 by Def1;
then consider V being Subset of X such that
A1: ( V is open & V c= U1 ) and
A2: x in V by TOPS_1:22;
reconsider V = V as non empty Subset of X by A2;
take V ; :: thesis: ( V is a_neighborhood of x & V is open & V c= U1 )
thus ( V is a_neighborhood of x & V is open & V c= U1 ) by A1, A2, Th3; :: thesis: verum