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

( A is closed iff for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A )

let A be Subset of T; :: thesis: ( A is closed iff for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A )

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

hence ( A is closed implies for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A ) by Th21; :: thesis: ( ( for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A ) implies A is closed )

assume A1: for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A ; :: thesis: A is closed

A = Cl A

( A is closed iff for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A )

let A be Subset of T; :: thesis: ( A is closed iff for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A )

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

hence ( A is closed implies for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A ) by Th21; :: thesis: ( ( for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N holds

x in A ) implies A is closed )

assume A1: for N being net of T st N is_eventually_in A holds

for x being Point of T st x is_a_cluster_point_of N 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 N being net of T st

( N is_eventually_in A & y is_a_cluster_point_of N ) by A2, Th21;

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 N being net of T st

( N is_eventually_in A & y is_a_cluster_point_of N ) by A2, Th21;

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