let T be non empty TopSpace; :: thesis: for N being net of T
for s being Point of T holds
( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )
let N be net of T; :: thesis: for s being Point of T holds
( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )
let s be Point of T; :: thesis: ( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )

hereby :: thesis: ( ( for A being Subset of T,N holds s in Cl A ) implies s is_a_cluster_point_of N )

assume A1: s is_a_cluster_point_of N ; :: thesis: for A being Subset of T,N holds s in Cl A
let A be Subset of T,N; :: thesis: s in Cl A
N is_eventually_in A by Th9;
hence s in Cl A by A1, Th23; :: thesis: verum

end;

assume A2: for A being Subset of T,N holds s in Cl A ; :: thesis: s is_a_cluster_point_of N
let V be a_neighborhood of s; :: according to WAYBEL_9:def 9 :: thesis: N is_often_in V
let i be Element of N; :: according to WAYBEL_0:def 12 :: thesis: ex b₁ being Element of the carrier of N st
( i <= b₁ & N . b₁ in V )
reconsider A = rng the mapping of (N | i) as Subset of T,N by Def2;
consider x being Element of A /\ (Int V);
( s in Int V & Int V is open & s in Cl A ) by A2, CONNSP_2:def 1;
then A meets Int V by PRE_TOPC:def 13;
then A /\ (Int V) <> {} T by XBOOLE_0:def 7;
then A3: ( x in A & x in Int V ) by XBOOLE_0:def 4;
then consider j being set such that
A4: ( j in dom the mapping of (N | i) & x = the mapping of (N | i) . j ) by FUNCT_1:def 5;
A5: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def 1;
reconsider j = j as Element of (N | i) by A4;
the carrier of (N | i) = { l where l is Element of N : i <= l } by WAYBEL_9:12;
then consider l being Element of N such that
A6: ( j = l & i <= l ) by A4, A5;
take l ; :: thesis: ( i <= l & N . l in V )
thus i <= l by A6; :: thesis: N . l in V
A7: x = (N | i) . j by A4
.= N . l by A6, WAYBEL_9:16 ;
Int V c= V by TOPS_1:44;
hence N . l in V by A3, A7; :: thesis: verum