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

ex A being Subset of X st

( A is a_neighborhood of x & A c= U1 ) ) by Th3; :: thesis: verum

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

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

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

hence
U1 is open
by TOPS_1:25; :: thesis: verum
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 )

A6: ( V c= U1 & x in V ) ; :: thesis: x in U1

thus x in U1 by A6; :: thesis: verum

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

given V being Subset of X such that
V is open
and
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;( 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

A6: ( V c= U1 & x in V ) ; :: thesis: x in U1

thus x in U1 by A6; :: thesis: verum

ex A being Subset of X st

( A is a_neighborhood of x & A c= U1 ) ) by Th3; :: thesis: verum