let T be non empty TopSpace; 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; ( 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 )
; ( ( 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
; 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
; 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; verum