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
proof
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;
hence A is closed ; :: thesis: verum