let X be non empty TopSpace; :: thesis: for x being Point of
for U1 being Subset of st U1 is a_neighborhood of x holds
ex V being non empty Subset of st
( V is a_neighborhood of x & V is open & V c= U1 )
let x be Point of ; :: thesis: for U1 being Subset of st U1 is a_neighborhood of x holds
ex V being non empty Subset of st
( V is a_neighborhood of x & V is open & V c= U1 )
let U1 be Subset of ; :: thesis: ( U1 is a_neighborhood of x implies ex V being non empty Subset of 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 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 such that
A1: ( V is open & V c= U1 ) and
A2: x in V by TOPS_1:54;
reconsider V = V as non empty Subset of 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, Th5; :: thesis: verum