let X be non empty TopSpace; :: thesis:
let U1 be Subset of X; :: thesis:

now :: thesis:

assume A1: for x being Point of X st x in U1 holds
ex A being Subset of X st
( A is a_neighborhood of x & A c= U1 ) ; :: thesis:
for x being set holds
( x in U1 iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) )

proof

let x be set ; :: thesis:
thus ( x in U1 implies ex V being Subset of X st
( V is open & V c= U1 & x in V ) ) :: thesis:

proof

assume A2: x in U1 ; :: thesis:
then reconsider x = x as Point of X ;
consider S being Subset of X such that
A3: S is a_neighborhood of x and
A4: S c= U1 by A1, A2;
consider V being Subset of X such that
A5: ( V is open & V c= S & x in V ) by A3, Th6;
take V ; :: thesis:
thus ( V is open & V c= U1 & x in V ) by A4, A5; :: thesis:

end;

given V being Subset of X such that V is open and
A6: ( V c= U1 & x in V ) ; :: thesis:
thus x in U1 by A6; :: thesis:

end;

hence U1 is open by TOPS_1:25; :: thesis:

end;

hence ( U1 is open iff for x being Point of X st x in U1 holds
ex A being Subset of X st
( A is a_neighborhood of x & A c= U1 ) ) by Th3; :: thesis: