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 ) )
hereby :: thesis: ( ex N being convergent net of T st
( 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;
given N being convergent net of T such that A4: N is_eventually_in A and
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