let T be non empty TopSpace; 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; 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; ( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )
thus
( s is_a_cluster_point_of N implies for A being Subset of T,N holds s in Cl A )
by Th8, Th21; ( ( for A being Subset of T,N holds s in Cl A ) implies s is_a_cluster_point_of N )
assume A1:
for A being Subset of T,N holds s in Cl A
; s is_a_cluster_point_of N
let V be a_neighborhood of s; WAYBEL_9:def 9 N is_often_in V
let i be Element of N; WAYBEL_0:def 12 ex b1 being Element of the carrier of N st
( i <= b1 & N . b1 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);
A2:
s in Int V
by CONNSP_2:def 1;
s in Cl A
by A1;
then
A meets Int V
by A2, PRE_TOPC:def 7;
then A3:
A /\ (Int V) <> {} T
;
then A4:
the Element of A /\ (Int V) in Int V
by XBOOLE_0:def 4;
A5:
Int V c= V
by TOPS_1:16;
the Element of A /\ (Int V) in A
by A3, XBOOLE_0:def 4;
then consider j being object such that
A6:
j in dom the mapping of (N | i)
and
A7:
the Element of A /\ (Int V) = the mapping of (N | i) . j
by FUNCT_1:def 3;
A8:
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 A6;
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
A9:
j = l
and
A10:
i <= l
by A6, A8;
take
l
; ( i <= l & N . l in V )
thus
i <= l
by A10; N . l in V
the Element of A /\ (Int V) =
(N | i) . j
by A7
.=
N . l
by A9, WAYBEL_9:16
;
hence
N . l in V
by A4, A5; verum