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

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