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 ) )

( V is open & V c= U1 & x in V ) ) by A1; :: thesis: verum

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 ) )

( 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;( 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

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 )

hence
( U1 is a_neighborhood of x iff 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;x in Int U1 by A3, TOPS_1:22;

hence U1 is a_neighborhood of x by Def1; :: thesis: verum

( V is open & V c= U1 & x in V ) ) by A1; :: thesis: verum