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

( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A )

let A be Subset of T; :: thesis: ( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A )

( A is closed iff Cl A = A ) by PRE_TOPC:22;

hence ( A is closed implies for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A ) by Th25; :: thesis: ( ( for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A ) implies A is closed )

assume A1: for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A ; :: thesis: A is closed

A = Cl A

( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A )

let A be Subset of T; :: thesis: ( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A )

( A is closed iff Cl A = A ) by PRE_TOPC:22;

hence ( A is closed implies for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A ) by Th25; :: thesis: ( ( for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A ) implies A is closed )

assume A1: for F being proper Filter of (BoolePoset ([#] T)) st A in F holds

for x being Point of T st x is_a_cluster_point_of F,T holds

x in A ; :: thesis: A is closed

A = Cl A

proof

hence
A is closed
; :: thesis: verum
thus
A c= Cl A
by PRE_TOPC:18; :: according to XBOOLE_0:def 10 :: thesis: Cl A c= A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in A )

assume A2: x in Cl A ; :: thesis: x in A

then reconsider y = x as Element of T ;

ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & y is_a_cluster_point_of F,T ) by A2, Th25;

hence x in A by A1; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in A )

assume A2: x in Cl A ; :: thesis: x in A

then reconsider y = x as Element of T ;

ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & y is_a_cluster_point_of F,T ) by A2, Th25;

hence x in A by A1; :: thesis: verum