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]
consider F being Function of the carrier of N, bool the carrier of T such that
A3:
for e being Element of N holds S1[e,F . e]
from FUNCT_2:sch 3(A1);
A4:
dom F = the carrier of N
by FUNCT_2:def 1;
reconsider RF = rng F as Subset-Family of T ;
A5:
RF is centered
proof
thus
RF <> {}
by A4, RELAT_1:65;
:: 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 = {} )
let H be
set ;
:: thesis: ( H = {} or not H c= RF or not H is finite or not meet H = {} )
assume that A6:
H <> {}
and A7:
H c= RF
and A8:
H is
finite
;
:: thesis: not meet H = {}
reconsider H1 =
H as non
empty set by A6;
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 ) } ;
consider e being
Element of
H1;
e in RF
by A7, TARSKI:def 3;
then consider x being
set such that A9:
x in dom F
and
e = F . x
by FUNCT_1:def 5;
reconsider x =
x as
Element of
N by A9;
consider X being
Subset of
T,
a being
Element of
N such that
a = x
and A10:
(
X = { (N . j) where j is Element of N : a <= j } &
F . x = Cl X )
by A3;
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 A10;
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 ;
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 );
A11:
for
e being
Element of
H1 ex
u being
Element of
J st
S2[
e,
u]
consider Q being
Function of
H1,
J such that A17:
for
e being
Element of
H1 holds
S2[
e,
Q . e]
from FUNCT_2:sch 3(A11);
dom Q = H
by FUNCT_2:def 1;
then A18:
rng Q is
finite
by A8, FINSET_1:26;
rng Q c= [#] N
then reconsider RQ =
rng Q as
Subset of
([#] N) ;
( not
[#] N is
empty &
[#] N is
directed )
by WAYBEL_0:def 6;
then consider i0 being
Element of
N such that
i0 in [#] N
and A22:
i0 is_>=_than RQ
by A18, WAYBEL_0:1;
for
Y being
set st
Y in H holds
N . i0 in Y
hence
meet H <> {}
by A6, SETFAM_1:def 1;
:: thesis: verum
end;
RF is closed
then
meet RF <> {}
by A5, COMPTS_1:13;
then consider c being set such that
A33:
c in meet RF
by XBOOLE_0:def 1;
reconsider c = c as Point of T by A33;
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
A34:
not N is_often_in O
by Def9;
N is_eventually_in the carrier of T \ O
by A34, WAYBEL_0:10;
then consider s0 being Element of N such that
A35:
for j being Element of N st s0 <= j holds
N . j in the carrier of T \ O
by WAYBEL_0:def 11;
consider Y being Subset of T, a being Element of N such that
A36:
a = s0
and
A37:
Y = { (N . j) where j is Element of N : a <= j }
and
A38:
F . s0 = Cl Y
by A3;
Cl Y in RF
by A4, A38, FUNCT_1:def 5;
then A39:
c in Cl Y
by A33, SETFAM_1:def 1;
{} = O /\ Y
then
O misses Y
by XBOOLE_0:def 7;
then A43:
Int O misses Y
by TOPS_1:44, XBOOLE_1:63;
A44:
Int O is open
by TOPS_1:51;
c in Int O
by CONNSP_2:def 1;
hence
contradiction
by A39, A43, A44, PRE_TOPC:def 13; :: thesis: verum