let X be non empty TopSpace; :: thesis: for x being Point of
for U1 being Subset of holds
( U1 is a_neighborhood of x iff ex V being Subset of st
( V is open & V c= U1 & x in V ) )
let x be Point of ; :: thesis: for U1 being Subset of holds
( U1 is a_neighborhood of x iff ex V being Subset of st
( V is open & V c= U1 & x in V ) )
let U1 be Subset of ; :: thesis: ( U1 is a_neighborhood of x iff ex V being Subset of st
( V is open & V c= U1 & x in V ) )

A1: now

assume U1 is a_neighborhood of x ; :: thesis: ex V being non empty Subset of ex V being Subset of st
( V is open & V c= U1 & x in V )
then consider V being non empty Subset of such that
A2: ( V is a_neighborhood of x & V is open & V c= U1 ) by Th7;
take V = V; :: thesis: ex V being Subset of st
( V is open & V c= U1 & x in V )
thus ex V being Subset of st
( V is open & V c= U1 & x in V ) by A2, Th6; :: thesis: verum

end;

now

given V being Subset of 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:54;
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 st
( V is open & V c= U1 & x in V ) ) by A1; :: thesis: verum