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