let T be non empty TopSpace; :: thesis: ( ( for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ) implies T is compact )
assume A1:
for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N
; :: thesis: T is compact
now let F be
Subset-Family of
T;
:: thesis: ( F is centered & F is closed implies meet F <> {} )assume A2:
(
F is
centered &
F is
closed )
;
:: thesis: meet F <> {} set G =
FinMeetCl F;
defpred S1[
set ,
set ]
means $2
in $1;
consider f being
Function such that A5:
(
dom f = FinMeetCl F &
rng f c= the
carrier of
T )
and A6:
for
a being
set st
a in FinMeetCl F holds
S1[
a,
f . a]
from WELLORD2:sch 1(A3);
A7:
(
F <> {} &
F c= FinMeetCl F )
by A2, CANTOR_1:4, FINSET_1:def 3;
then reconsider G =
FinMeetCl F as non
empty Subset-Family of
T ;
set R =
(InclPoset G) opp ;
A8:
InclPoset G = RelStr(#
G,
(RelIncl G) #)
by YELLOW_1:def 1;
then A9:
the
carrier of
((InclPoset G) opp ) = G
by YELLOW_6:12;
(InclPoset G) opp is
directed
then reconsider R =
(InclPoset G) opp as non
empty transitive directed RelStr ;
reconsider f =
f as
Function of the
carrier of
R,the
carrier of
T by A5, A9, FUNCT_2:4;
set N =
R *' f;
A12:
(
RelStr(# the
carrier of
(R *' f),the
InternalRel of
(R *' f) #)
= RelStr(# the
carrier of
R,the
InternalRel of
R #) & the
mapping of
(R *' f) = f )
by WAYBEL32:def 3;
set X = the
carrier of
T;
A13:
the_universe_of the
carrier of
T = Tarski-Class (the_transitive-closure_of the carrier of T)
by YELLOW_6:def 3;
( the
carrier of
T c= the_transitive-closure_of the
carrier of
T &
the_transitive-closure_of the
carrier of
T in Tarski-Class (the_transitive-closure_of the carrier of T) )
by CLASSES1:5, CLASSES1:59;
then
the
carrier of
T in Tarski-Class (the_transitive-closure_of the carrier of T)
by CLASSES1:6;
then
bool the
carrier of
T in Tarski-Class (the_transitive-closure_of the carrier of T)
by CLASSES1:7;
then
G in Tarski-Class (the_transitive-closure_of the carrier of T)
by CLASSES1:6;
then
R *' f in NetUniv T
by A9, A12, A13, YELLOW_6:def 14;
then consider x being
Point of
T such that A14:
x is_a_cluster_point_of R *' f
by A1;
now let X be
set ;
:: thesis: ( X in F implies x in X )assume A15:
X in F
;
:: thesis: x in Xthen reconsider a =
X as
Element of
(R *' f) by A7, A8, A12, YELLOW_6:12;
reconsider A =
X as
Subset of
T by A15;
A is
closed
by A2, A15, TOPS_2:def 2;
then A16:
Cl A = A
by PRE_TOPC:52;
now let V be
Subset of
T;
:: thesis: ( V is open & x in V implies A meets V )assume A17:
(
V is
open &
x in V )
;
:: thesis: A meets Vthen
Int V = V
by TOPS_1:55;
then
V is
a_neighborhood of
x
by A17, CONNSP_2:def 1;
then
R *' f is_often_in V
by A14, WAYBEL_9:def 9;
then consider b being
Element of
(R *' f) such that A18:
(
a <= b &
(R *' f) . b in V )
by WAYBEL_0:def 12;
reconsider a' =
a,
b' =
b as
Element of
((InclPoset G) opp ) by A12;
a' <= b'
by A12, A18, YELLOW_0:1;
then
(
~ a' >= ~ b' &
~ a' = A &
~ b' = b )
by LATTICE3:def 7, YELLOW_7:1;
then
(
b c= A &
(R *' f) . b in b )
by A6, A8, A12, YELLOW_1:3;
hence
A meets V
by A18, XBOOLE_0:3;
:: thesis: verum end; hence
x in X
by A16, PRE_TOPC:def 13;
:: thesis: verum end; hence
meet F <> {}
by A7, SETFAM_1:def 1;
:: thesis: verum end;
hence
T is compact
by COMPTS_1:13; :: thesis: verum