let T be non empty Hausdorff compact TopSpace; :: thesis:
let N be net of T; :: thesis:
defpred S₁[ 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 S₁[e,u]

let e be Element of N; :: thesis:
reconsider a = e as Element of N ;
{ (N . j) where j is Element of N : a <= j } c= the carrier of T

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in { (N . j) where j is Element of N : a <= j } ; :: thesis:
then ex j being Element of N st
( q = N . j & a <= j ) ;
hence q in the carrier of T ; :: thesis:

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:
take X ; :: thesis:
take a ; :: thesis:
thus ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X ) ; :: thesis:

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 S₁[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

thus RF <> {} by A3, RELAT_1:42; :: according to FINSET_1:def 3 :: thesis:
defpred S₂[ 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:
assume that
A5: H <> {} and
A6: H c= RF and
A7: H is finite ; :: thesis:
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 S₂[e,u]

let e be Element of H1; :: thesis:
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:
take i = x; :: thesis:
take h = X; :: thesis:
take Ch = Cl X; :: thesis:
thus i = u by A13; :: thesis:
thus Ch = e by A12, A15; :: thesis:
thus h = { (N . j) where j is Element of N : i <= j } by A13, A14; :: thesis:
thus Ch = Cl h ; :: thesis:

end;

consider Q being Function of H1,J such that
A16: for e being Element of H1 holds S₂[e,Q . e] from FUNCT_2:sch 3(A10);
rng Q c= [#] N

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in rng Q ; :: thesis:
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:

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

let Y be set ; :: thesis:
assume A21: Y in H ; :: thesis:
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:

end;

end;

let P be Subset of T; :: according to TOPS_2:def 2 :: thesis:
assume P in RF ; :: thesis:
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:

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:
assume not c is_a_cluster_point_of N ; :: thesis:
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

end;