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 ) by WAYBEL_7:def 5; :: 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
consider x being Element of A \ (Int A);
assume not A is open ; :: thesis: contradiction
then ( A <> Int A & Int A c= A ) by TOPS_1:44;
then not A c= Int A by XBOOLE_0:def 10;
then A2: A \ (Int A) <> {} by XBOOLE_1:37;
then x in A \ (Int A) ;
then reconsider x = x as Point of T ;
( x is_a_convergence_point_of NeighborhoodSystem x,T & x in A ) by A2, Th4, XBOOLE_0:def 5;
then A in NeighborhoodSystem x by A1;
then A is a_neighborhood of x by Th3;
then x in Int A by CONNSP_2:def 1;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum