let T be non empty Hausdorff compact TopSpace; :: thesis: for N being net of T ex c being Point of T st c is_a_cluster_point_of N
let N be net of T; :: thesis: ex c being Point of T st c is_a_cluster_point_of N
defpred S1[ set , set ] means ex X being Subset of T ex a being Element of N st
( a = $1 & X = { (N . j) where j is Element of N : a <= j } & $2 = Cl X );
A1: for e being Element of N ex u being Subset of T st S1[e,u]
proof
let e be Element of N; :: thesis: ex u being Subset of T st S1[e,u]
reconsider a = e as Element of N ;
{ (N . j) where j is Element of N : a <= j } c= the carrier of T
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (N . j) where j is Element of N : a <= j } or q in the carrier of T )
assume q in { (N . j) where j is Element of N : a <= j } ; :: thesis: q in the carrier of T
then ex j being Element of N st
( q = N . j & a <= j ) ;
hence q in the carrier of T ; :: thesis: verum
end;
then reconsider X = { (N . j) where j is Element of N : a <= j } as Subset of the carrier of T ;
take Cl X ; :: thesis: S1[e, Cl X]
take X ; :: thesis: ex a being Element of N st
( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X )
take a ; :: thesis: ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X )
thus ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X ) ; :: thesis: verum
end;
consider F being Function of the carrier of N,(bool the carrier of T) such that
A2: for e being Element of N holds S1[e,F . e] from FUNCT_2:sch 3(A1);
 reconsider RF = rng F as Subset-Family of T ;
A3: dom F = the carrier of N by FUNCT_2:def 1;
A4: RF is centered
proof
thus RF <> {} by A3, RELAT_1:42; :: according to FINSET_1:def 3 :: thesis: for b1 being set holds
( b1 = {} or not b1 c= RF or not b1 is finite or not meet b1 = {} )
defpred S2[ set , set ] means ex i being Element of N ex h, Ch being Subset of T st
( i = $2 & Ch = $1 & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h );
set J = { i where i is Element of N : ex h, Ch being Subset of T st
( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } ;
let H be set ; :: thesis: ( H = {} or not H c= RF or not H is finite or not meet H = {} )
assume that
A5: H <> {} and
A6: H c= RF and
A7: H is finite ; :: thesis: not meet H = {}
reconsider H1 = H as non empty set by A5;
set e = the Element of H1;
the Element of H1 in RF by A6;
then consider x being object such that
A8: x in dom F and
the Element of H1 = F . x by FUNCT_1:def 3;
reconsider x = x as Element of N by A8;
consider X being Subset of T, a being Element of N such that
a = x and
A9: ( X = { (N . j) where j is Element of N : a <= j } & F . x = Cl X ) by A2;
a in { i where i is Element of N : ex h, Ch being Subset of T st
( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } by A9;
then reconsider J = { i where i is Element of N : ex h, Ch being Subset of T st
( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } as non empty set ;
A10: for e being Element of H1 ex u being Element of J st S2[e,u]
proof
let e be Element of H1; :: thesis: ex u being Element of J st S2[e,u]
e in RF by A6;
then consider x being object such that
A11: x in dom F and
A12: e = F . x by FUNCT_1:def 3;
reconsider x = x as Element of N by A11;
consider X being Subset of T, a being Element of N such that
A13: a = x and
A14: X = { (N . j) where j is Element of N : a <= j } and
A15: F . x = Cl X by A2;
a in J by A14, A15;
then reconsider a = a as Element of J ;
take u = a; :: thesis: S2[e,u]
take i = x; :: thesis: ex h, Ch being Subset of T st
( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
take h = X; :: thesis: ex Ch being Subset of T st
( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
take Ch = Cl X; :: thesis: ( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
thus i = u by A13; :: thesis: ( Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
thus Ch = e by A12, A15; :: thesis: ( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
thus h = { (N . j) where j is Element of N : i <= j } by A13, A14; :: thesis: Ch = Cl h
thus Ch = Cl h ; :: thesis: verum
end;
consider Q being Function of H1,J such that
A16: for e being Element of H1 holds S2[e,Q . e] from FUNCT_2:sch 3(A10);
 rng Q c= [#] N
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng Q or q in [#] N )
assume q in rng Q ; :: thesis: q in [#] N
then consider x being object such that
A17: x in dom Q and
A18: Q . x = q by FUNCT_1:def 3;
reconsider x = x as Element of H1 by A17;
ex i being Element of N ex h, Ch being Subset of T st
( i = Q . x & Ch = x & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) by A16;
hence q in [#] N by A18; :: thesis: verum
end;
then reconsider RQ = rng Q as Subset of ([#] N) ;
A19: ( not [#] N is empty & [#] N is directed ) by WAYBEL_0:def 6;
dom Q = H by FUNCT_2:def 1;
then rng Q is finite by A7, FINSET_1:8;
then consider i0 being Element of N such that
i0 in [#] N and
A20: i0 is_>=_than RQ by A19, WAYBEL_0:1;
for Y being set st Y in H holds
N . i0 in Y
proof
let Y be set ; :: thesis: ( Y in H implies N . i0 in Y )
assume A21: Y in H ; :: thesis: N . i0 in Y
then consider i being Element of N, h, Ch being Subset of T such that
A22: i = Q . Y and
A23: Ch = Y and
A24: h = { (N . j) where j is Element of N : i <= j } and
A25: Ch = Cl h by A16;
Y in dom Q by A21, FUNCT_2:def 1;
then i in rng Q by A22, FUNCT_1:def 3;
then i <= i0 by A20;
then A26: N . i0 in h by A24;
h c= Cl h by PRE_TOPC:18;
hence N . i0 in Y by A23, A25, A26; :: thesis: verum
end;
hence not meet H = {} by A5, SETFAM_1:def 1; :: thesis: verum
end;
RF is closed
proof
let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not P in RF or P is closed )
assume P in RF ; :: thesis: P is closed
then consider x being object such that
A27: x in dom F and
A28: F . x = P by FUNCT_1:def 3;
reconsider x = x as Element of N by A27;
ex X being Subset of T ex a being Element of N st
( a = x & X = { (N . j) where j is Element of N : a <= j } & F . x = Cl X ) by A2;
then P = Cl P by A28;
hence P is closed ; :: thesis: verum
end;
then meet RF <> {} by A4, COMPTS_1:4;
then consider c being object such that
A29: c in meet RF by XBOOLE_0:def 1;
reconsider c = c as Point of T by A29;
take c ; :: thesis: c is_a_cluster_point_of N
assume not c is_a_cluster_point_of N ; :: thesis: contradiction
then consider O being a_neighborhood of c such that
A30: not N is_often_in O ;
N is_eventually_in the carrier of T \ O by A30, WAYBEL_0:10;
then consider s0 being Element of N such that
A31: for j being Element of N st s0 <= j holds
N . j in the carrier of T \ O ;
consider Y being Subset of T, a being Element of N such that
A32: ( a = s0 & Y = { (N . j) where j is Element of N : a <= j } ) and
A33: F . s0 = Cl Y by A2;
Cl Y in RF by A3, A33, FUNCT_1:def 3;
then A34: c in Cl Y by A29, SETFAM_1:def 1;
{} = O /\ Y
proof
thus {} c= O /\ Y ; :: according to XBOOLE_0:def 10 :: thesis: O /\ Y c= {}
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in O /\ Y or q in {} )
assume A35: q in O /\ Y ; :: thesis: q in {}
q in Y by A35, XBOOLE_0:def 4;
then consider j being Element of N such that
A36: q = N . j and
A37: s0 <= j by A32;
assume not q in {} ; :: thesis: contradiction
N . j in the carrier of T \ O by A31, A37;
then not N . j in O by XBOOLE_0:def 5;
hence contradiction by A35, A36, XBOOLE_0:def 4; :: thesis: verum
end;
then O misses Y ;
then A38: Int O misses Y by TOPS_1:16, XBOOLE_1:63;
( Int O is open & c in Int O ) by CONNSP_2:def 1;
hence contradiction by A34, A38, PRE_TOPC:def 7; :: thesis: verum