let T be non empty TopSpace; ( 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
; 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; 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
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 S1[
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 <> {}
;
FINSET_1:def 3 for b1 being set holds
( b1 = {} or not b1 c= F or not b1 is finite or not meet b1 = {} )
let G be
set ;
( 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
;
not meet G = {}
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
S1[
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 for X being set st X in G holds
N . j in Xlet X be
set ;
( X in G implies N . j in X )assume A12:
X in G
;
N . j in Xthen 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;
verum end;
hence
not
meet G = {}
by A3, SETFAM_1:def 1;
verum
end;
F is closed
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
; x is_a_cluster_point_of N
hence
x is_a_cluster_point_of N
by Th29; verum