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;
set x = the Element of A /\ (Int V);
A3: s in Int V by CONNSP_2:def 1;
s in Cl A by A2;
then A meets Int V by A3, PRE_TOPC:def 7;
then A4: A /\ (Int V) <> {} T by XBOOLE_0:def 7;
then A5: the Element of A /\ (Int V) in Int V by XBOOLE_0:def 4;
A6: Int V c= V by TOPS_1:16;
the Element of A /\ (Int V) in A by A4, XBOOLE_0:def 4;
then consider j being set such that
A7: j in dom the mapping of (N | i) and
A8: the Element of A /\ (Int V) = the mapping of (N | i) . j by FUNCT_1:def 3;
A9: the carrier of (N | i) = { l where l is Element of N : i <= l } by WAYBEL_9:12;
reconsider j = j as Element of (N | i) by A7;
dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def 1;
then consider l being Element of N such that
A10: j = l and
A11: i <= l by A7, A9;
take l ; :: thesis: ( i <= l & N . l in V )
thus i <= l by A11; :: thesis: N . l in V
the Element of A /\ (Int V) = (N | i) . j by A8
.= N . l by A10, WAYBEL_9:16 ;
hence N . l in V by A5, A6; :: thesis: verum