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

set x = the Element of meet F;

A2: F is centered

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

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

then reconsider F = { (Cl A) where A is Subset of T,N : verum } as Subset-Family of T ;
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;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

set x = the Element of meet F;

A2: F is centered

proof

F is closed
defpred S_{1}[ 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_{1} being set holds

( b_{1} = {} or not b_{1} c= F or not b_{1} is finite or not meet b_{1} = {} )

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 = {}

A9: ( dom f = G & rng f c= the carrier of N ) and

A10: for x being object st x in G holds

S_{1}[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;

end;( $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

( 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_{1}[x,y] )

consider f being Function such that ex y being object st

( y in the carrier of N & S

let x be object ; :: thesis: ( x in G implies ex y being object st

( y in the carrier of N & S_{1}[x,y] ) )

assume x in G ; :: thesis: ex y being object st

( y in the carrier of N & S_{1}[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_{1}[x,y] )

thus y in the carrier of N ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A7, A8; :: thesis: verum

end;( y in the carrier of N & S

assume x in G ; :: thesis: ex y being object st

( y in the carrier of N & S

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

thus y in the carrier of N ; :: thesis: S

thus S

A9: ( dom f = G & rng f c= the carrier of N ) and

A10: for x being object st x in G holds

S

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

hence
not meet G = {}
by A3, SETFAM_1:def 1; :: thesis: verumN . 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;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

proof

then A19:
meet F <> {}
by A1, A2, COMPTS_1:4;
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;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

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

hence
x is_a_cluster_point_of N
by Th29; :: thesis: verumlet 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;Cl A in F ;

hence x in Cl A by A19, SETFAM_1:def 1; :: thesis: verum