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

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F )

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

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F )

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

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F ) ; :: thesis: ( ( for x being Point of T st x in A holds

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F ) implies A is open )

assume A1: for x being Point of T st x in A holds

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F ; :: thesis: A is open

set x = the Element of A \ (Int A);

A2: Int A c= A by TOPS_1:16;

assume not A is open ; :: thesis: contradiction

then not A c= Int A by A2, XBOOLE_0:def 10;

then A3: A \ (Int A) <> {} by XBOOLE_1:37;

then the Element of A \ (Int A) in A \ (Int A) ;

then reconsider x = the Element of A \ (Int A) as Point of T ;

A4: x in A by A3, XBOOLE_0:def 5;

x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;

then A in NeighborhoodSystem x by A1, A4;

then A is a_neighborhood of x by Th2;

then x in Int A by CONNSP_2:def 1;

hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum

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

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F )

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

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F )

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

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F ) ; :: thesis: ( ( for x being Point of T st x in A holds

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F ) implies A is open )

assume A1: for x being Point of T st x in A holds

for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds

A in F ; :: thesis: A is open

set x = the Element of A \ (Int A);

A2: Int A c= A by TOPS_1:16;

assume not A is open ; :: thesis: contradiction

then not A c= Int A by A2, XBOOLE_0:def 10;

then A3: A \ (Int A) <> {} by XBOOLE_1:37;

then the Element of A \ (Int A) in A \ (Int A) ;

then reconsider x = the Element of A \ (Int A) as Point of T ;

A4: x in A by A3, XBOOLE_0:def 5;

x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;

then A in NeighborhoodSystem x by A1, A4;

then A is a_neighborhood of x by Th2;

then x in Int A by CONNSP_2:def 1;

hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum