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 and
A2: V c= U1 and
A3: x in V by TOPS_1:54;
reconsider V = V as non empty Subset of X by A3;
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, A3, Th5; :: thesis: verum