let X be non empty TopSpace; :: thesis: for x being Point of X
for U1 being Subset of X holds
( U1 is a_neighborhood of x iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) )
let x be Point of X; :: thesis: for U1 being Subset of X holds
( U1 is a_neighborhood of x iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) )
let U1 be Subset of X; :: thesis: ( U1 is a_neighborhood of x iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) )
A1: now :: thesis: ( U1 is a_neighborhood of x implies ex V being non empty Subset of X ex V being Subset of X st
( V is open & V c= U1 & x in V ) )
assume U1 is a_neighborhood of x ; :: thesis: ex V being non empty Subset of X ex V being Subset of X st
( V is open & V c= U1 & x in V )
then consider V being non empty Subset of X such that
A2: ( V is a_neighborhood of x & V is open & V c= U1 ) by Th5;
take V = V; :: thesis: ex V being Subset of X st
( V is open & V c= U1 & x in V )
thus ex V being Subset of X st
( V is open & V c= U1 & x in V ) by A2, Th4; :: thesis: verum
end;
now :: thesis: ( ex V being Subset of X st
( V is open & V c= U1 & x in V ) implies U1 is a_neighborhood of x )
given V being Subset of X such that A3: ( V is open & V c= U1 & x in V ) ; :: thesis: U1 is a_neighborhood of x
x in Int U1 by A3, TOPS_1:22;
hence U1 is a_neighborhood of x by Def1; :: thesis: verum
end;
hence ( U1 is a_neighborhood of x iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) ) by A1; :: thesis: verum