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 )

thus ( s is_a_cluster_point_of N implies for A being Subset of T,N holds s in Cl A ) by Th8, Th21; :: thesis: ( ( 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 ; :: 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_{1} being Element of the carrier of N st

( i <= b_{1} & N . b_{1} 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 ; :: thesis: ( i <= l & N . l in V )

thus i <= l by A10; :: thesis: 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; :: thesis: verum

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 )

thus ( s is_a_cluster_point_of N implies for A being Subset of T,N holds s in Cl A ) by Th8, Th21; :: thesis: ( ( 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 ; :: 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

( i <= b

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 ; :: thesis: ( i <= l & N . l in V )

thus i <= l by A10; :: thesis: 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; :: thesis: verum