let T be non empty TopSpace; :: thesis: ( T is compact implies for N being net of T ex x being Point of T st x is_a_cluster_point_of N )
assume A1: T is compact ; :: thesis: for N being net of T ex x being Point of T st x is_a_cluster_point_of N
let N be net of T; :: thesis: ex x being Point of T st x is_a_cluster_point_of N
set F = { (Cl A) where A is Subset of T,N : verum } ;
{ (Cl A) where A is Subset of T,N : verum } c= bool the carrier of T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Cl A) where A is Subset of T,N : verum } or x in bool the carrier of T )
assume x in { (Cl A) where A is Subset of T,N : verum } ; :: thesis: x in bool the carrier of T
then ex A being Subset of T,N st x = Cl A ;
hence x in bool the carrier of T ; :: thesis: verum

end;

then reconsider F = { (Cl A) where A is Subset of T,N : verum } as Subset-Family of T ;
set x = the Element of meet F;
A2: F is centered

proof

defpred S₁[ object , object ] means ex A being Subset of T,N ex i being Element of N st
( $1 = Cl A & $2 = i & A = rng the mapping of (N | i) );
set A0 = the Subset of T,N;
Cl the Subset of T,N in F ;
hence F <> {} ; :: according to FINSET_1:def 3 :: thesis: for b₁ being set holds
( b₁ = {} or not b₁ c= F or not b₁ is finite or not meet b₁ = {} )
let G be set ; :: thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} )
assume that
A3: G <> {} and
A4: G c= F and
A5: G is finite ; :: thesis: not meet G = {}

A6: now :: thesis: for x being object st x in G holds
ex y being object st
( y in the carrier of N & S₁[x,y] )

let x be object ; :: thesis: ( x in G implies ex y being object st
( y in the carrier of N & S₁[x,y] ) )
assume x in G ; :: thesis: ex y being object st
( y in the carrier of N & S₁[x,y] )
then x in F by A4;
then consider A being Subset of T,N such that
A7: x = Cl A ;
consider i being Element of N such that
A8: A = rng the mapping of (N | i) by Def2;
reconsider y = i as object ;
take y = y; :: thesis: ( y in the carrier of N & S₁[x,y] )
thus y in the carrier of N ; :: thesis: S₁[x,y]
thus S₁[x,y] by A7, A8; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = G & rng f c= the carrier of N ) and
A10: for x being object st x in G holds
S₁[x,f . x] from FUNCT_1:sch 6(A6);
reconsider B = rng f as finite Subset of N by A5, A9, FINSET_1:8;
[#] N is directed by WAYBEL_0:def 6;
then consider j being Element of N such that
j in [#] N and
A11: j is_>=_than B by WAYBEL_0:1;

now :: thesis: for X being set st X in G holds
N . j in X

let X be set ; :: thesis: ( X in G implies N . j in X )
assume A12: X in G ; :: thesis: N . j in X
then consider A being Subset of T,N, i being Element of N such that
A13: X = Cl A and
A14: f . X = i and
A15: A = rng the mapping of (N | i) by A10;
A16: A c= X by A13, PRE_TOPC:18;
A17: the mapping of (N | i) = the mapping of N | the carrier of (N | i) by WAYBEL_9:def 7;
i in B by A9, A12, A14, FUNCT_1:def 3;
then i <= j by A11, LATTICE3:def 9;
then j in the carrier of (N | i) by WAYBEL_9:def 7;
then A18: j in dom the mapping of (N | i) by FUNCT_2:def 1;
then the mapping of (N | i) . j in A by A15, FUNCT_1:def 3;
then N . j in A by A18, A17, FUNCT_1:47;
hence N . j in X by A16; :: thesis: verum

end;

hence not meet G = {} by A3, SETFAM_1:def 1; :: thesis: verum

end;

F is closed

proof

let S be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not S in F or S is closed )
assume S in F ; :: thesis: S is closed
then ex A being Subset of T,N st S = Cl A ;
hence S is closed ; :: thesis: verum

end;

then A19: meet F <> {} by A1, A2, COMPTS_1:4;
then the Element of meet F in meet F ;
then reconsider x = the Element of meet F as Point of T ;
take x ; :: thesis: x is_a_cluster_point_of N

now :: thesis: for A being Subset of T,N holds x in Cl A

let A be Subset of T,N; :: thesis: x in Cl A
Cl A in F ;
hence x in Cl A by A19, SETFAM_1:def 1; :: thesis: verum

end;

hence x is_a_cluster_point_of N by Th29; :: thesis: verum