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

for x being Point of T holds

( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

let A be Subset of T; :: thesis: for x being Point of T holds

( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

let x be Point of T; :: thesis: ( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

A5: x in Lim N ; :: thesis: x in Cl A

x is_a_cluster_point_of N by A5, WAYBEL_9:29;

hence x in Cl A by A4, Th21; :: thesis: verum

for x being Point of T holds

( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

let A be Subset of T; :: thesis: for x being Point of T holds

( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

let x be Point of T; :: thesis: ( x in Cl A iff ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) )

hereby :: thesis: ( ex N being convergent net of T st

( N is_eventually_in A & x in Lim N ) implies x in Cl A )

given N being convergent net of T such that A4:
N is_eventually_in A
and ( N is_eventually_in A & x in Lim N ) implies x in Cl A )

assume
x in Cl A
; :: thesis: ex S being convergent net of T st

( S is_eventually_in A & x in Lim S )

then consider N being net of T such that

A1: N is_eventually_in A and

A2: x is_a_cluster_point_of N by Th21;

consider S being subnet of N such that

A3: x in Lim S by A2, WAYBEL_9:32;

reconsider S = S as convergent net of T by A3, YELLOW_6:def 16;

take S = S; :: thesis: ( S is_eventually_in A & x in Lim S )

thus S is_eventually_in A by A1, Th19; :: thesis: x in Lim S

thus x in Lim S by A3; :: thesis: verum

end;( S is_eventually_in A & x in Lim S )

then consider N being net of T such that

A1: N is_eventually_in A and

A2: x is_a_cluster_point_of N by Th21;

consider S being subnet of N such that

A3: x in Lim S by A2, WAYBEL_9:32;

reconsider S = S as convergent net of T by A3, YELLOW_6:def 16;

take S = S; :: thesis: ( S is_eventually_in A & x in Lim S )

thus S is_eventually_in A by A1, Th19; :: thesis: x in Lim S

thus x in Lim S by A3; :: thesis: verum

A5: x in Lim N ; :: thesis: x in Cl A

x is_a_cluster_point_of N by A5, WAYBEL_9:29;

hence x in Cl A by A4, Th21; :: thesis: verum