let T be non empty TopSpace; :: thesis: for A being Subset of T holds

( A is open iff for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A )

let A be Subset of T; :: thesis: ( A is open iff for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A )

thus ( A is open implies for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A ) :: thesis: ( ( for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A ) implies A is open )

ex B being Nbhd of x,T st B c= A ; :: thesis: A is open

for x being Point of T st x in A holds

ex B being Subset of T st

( B is a_neighborhood of x & B c= A )

( A is open iff for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A )

let A be Subset of T; :: thesis: ( A is open iff for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A )

thus ( A is open implies for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A ) :: thesis: ( ( for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A ) implies A is open )

proof

assume A2:
for x being Point of T st x in A holds
assume A1:
A is open
; :: thesis: for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A

let x be Point of T; :: thesis: ( x in A implies ex B being Nbhd of x,T st B c= A )

assume x in A ; :: thesis: ex B being Nbhd of x,T st B c= A

then ex B being Subset of T st

( B is a_neighborhood of x & B c= A ) by A1, CONNSP_2:7;

hence ex B being Nbhd of x,T st B c= A ; :: thesis: verum

end;ex B being Nbhd of x,T st B c= A

let x be Point of T; :: thesis: ( x in A implies ex B being Nbhd of x,T st B c= A )

assume x in A ; :: thesis: ex B being Nbhd of x,T st B c= A

then ex B being Subset of T st

( B is a_neighborhood of x & B c= A ) by A1, CONNSP_2:7;

hence ex B being Nbhd of x,T st B c= A ; :: thesis: verum

ex B being Nbhd of x,T st B c= A ; :: thesis: A is open

for x being Point of T st x in A holds

ex B being Subset of T st

( B is a_neighborhood of x & B c= A )

proof

hence
A is open
by CONNSP_2:7; :: thesis: verum
let x be Point of T; :: thesis: ( x in A implies ex B being Subset of T st

( B is a_neighborhood of x & B c= A ) )

assume x in A ; :: thesis: ex B being Subset of T st

( B is a_neighborhood of x & B c= A )

then ex B being Nbhd of x,T st B c= A by A2;

hence ex B being Subset of T st

( B is a_neighborhood of x & B c= A ) ; :: thesis: verum

end;( B is a_neighborhood of x & B c= A ) )

assume x in A ; :: thesis: ex B being Subset of T st

( B is a_neighborhood of x & B c= A )

then ex B being Nbhd of x,T st B c= A by A2;

hence ex B being Subset of T st

( B is a_neighborhood of x & B c= A ) ; :: thesis: verum