let X be non empty TopSpace; :: thesis: for U1 being Subset of X holds
( 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 ) )
let U1 be Subset of X; :: thesis: ( 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 ) )

now :: thesis: ( ( 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 ) ) implies U1 is open )

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: U1 is open
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: ( x in U1 iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) )
thus ( x in U1 implies ex V being Subset of X st
( V is open & V c= U1 & x in V ) ) :: thesis: ( ex V being Subset of X st
( V is open & V c= U1 & x in V ) implies x in U1 )

proof

assume A2: x in U1 ; :: thesis: ex V being Subset of X st
( V is open & V c= U1 & x in V )
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: ( V is open & V c= U1 & x in V )
thus ( V is open & V c= U1 & x in V ) by A4, A5; :: thesis: verum

end;

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

end;

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

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: verum