let T be non empty TopSpace; ( ( 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
; T is compact
now for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} set X = the
carrier of
T;
defpred S1[
object ,
object ]
means ex
A being
set st
(
A = $1 & $2
in A );
let F be
Subset-Family of
T;
( F is centered & F is closed implies meet F <> {} )assume that A2:
F is
centered
and A3:
F is
closed
;
meet F <> {} set G =
FinMeetCl F;
consider f being
Function such that A8:
(
dom f = FinMeetCl F &
rng f c= the
carrier of
T )
and A9:
for
a being
object st
a in FinMeetCl F holds
S1[
a,
f . a]
from FUNCT_1:sch 6(A4);
A10:
F c= FinMeetCl F
by CANTOR_1:4;
A11:
F <> {}
by A2;
then reconsider G =
FinMeetCl F as non
empty Subset-Family of
T by A10;
set R =
(InclPoset G) opp ;
A12:
InclPoset G = RelStr(#
G,
(RelIncl G) #)
by YELLOW_1:def 1;
then A13:
the
carrier of
((InclPoset G) opp) = G
by YELLOW_6:3;
(InclPoset G) opp is
directed
proof
let x,
y be
Element of
((InclPoset G) opp);
WAYBEL_0:def 1,
WAYBEL_0:def 6 ( not x in [#] ((InclPoset G) opp) or not y in [#] ((InclPoset G) opp) or ex b1 being Element of the carrier of ((InclPoset G) opp) st
( b1 in [#] ((InclPoset G) opp) & x <= b1 & y <= b1 ) )
assume that
x in [#] ((InclPoset G) opp)
and
y in [#] ((InclPoset G) opp)
;
ex b1 being Element of the carrier of ((InclPoset G) opp) st
( b1 in [#] ((InclPoset G) opp) & x <= b1 & y <= b1 )
A14:
~ x = x
by LATTICE3:def 7;
y in G
by A13;
then consider Y being
Subset-Family of
T such that A15:
Y c= F
and A16:
Y is
finite
and A17:
y = Intersect Y
by CANTOR_1:def 3;
x in G
by A13;
then consider X being
Subset-Family of
T such that A18:
X c= F
and A19:
X is
finite
and A20:
x = Intersect X
by CANTOR_1:def 3;
set z =
Intersect (X \/ Y);
X \/ Y c= F
by A18, A15, XBOOLE_1:8;
then reconsider z =
Intersect (X \/ Y) as
Element of
((InclPoset G) opp) by A13, A19, A16, CANTOR_1:def 3;
A21:
~ z = z
by LATTICE3:def 7;
take
z
;
( z in [#] ((InclPoset G) opp) & x <= z & y <= z )
thus
z in [#] ((InclPoset G) opp)
;
( x <= z & y <= z )
A22:
~ y = y
by LATTICE3:def 7;
z c= y
by A17, SETFAM_1:44, XBOOLE_1:7;
then A23:
~ z <= ~ y
by A22, A21, YELLOW_1:3;
z c= x
by A20, SETFAM_1:44, XBOOLE_1:7;
then
~ z <= ~ x
by A14, A21, YELLOW_1:3;
hence
(
x <= z &
y <= z )
by A23, YELLOW_7:1;
verum
end; 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 A8, A13, FUNCT_2:2;
set N =
R *' f;
A24:
RelStr(# the
carrier of
(R *' f), the
InternalRel of
(R *' f) #)
= RelStr(# the
carrier of
R, the
InternalRel of
R #)
by WAYBEL32:def 3;
A25:
the_universe_of the
carrier of
T = Tarski-Class (the_transitive-closure_of the carrier of T)
by YELLOW_6:def 1;
the
carrier of
T c= the_transitive-closure_of the
carrier of
T
by CLASSES1:52;
then
the
carrier of
T in Tarski-Class (the_transitive-closure_of the carrier of T)
by CLASSES1:2, CLASSES1:3;
then
bool the
carrier of
T in Tarski-Class (the_transitive-closure_of the carrier of T)
by CLASSES1:4;
then
G in Tarski-Class (the_transitive-closure_of the carrier of T)
by CLASSES1:3;
then
R *' f in NetUniv T
by A13, A24, A25, YELLOW_6:def 11;
then consider x being
Point of
T such that A26:
x is_a_cluster_point_of R *' f
by A1;
A27:
the
mapping of
(R *' f) = f
by WAYBEL32:def 3;
now for X being set st X in F holds
x in Xlet X be
set ;
( X in F implies x in X )assume A28:
X in F
;
x in Xthen reconsider A =
X as
Subset of
T ;
reconsider a =
X as
Element of
(R *' f) by A10, A12, A24, A28, YELLOW_6:3;
A29:
now for V being Subset of T st V is open & x in V holds
A meets Vlet V be
Subset of
T;
( V is open & x in V implies A meets V )assume that A30:
V is
open
and A31:
x in V
;
A meets V
Int V = V
by A30, TOPS_1:23;
then
V is
a_neighborhood of
x
by A31, CONNSP_2:def 1;
then
R *' f is_often_in V
by A26;
then consider b being
Element of
(R *' f) such that A32:
a <= b
and A33:
(R *' f) . b in V
;
reconsider a9 =
a,
b9 =
b as
Element of
((InclPoset G) opp) by A24;
a9 <= b9
by A24, A32, YELLOW_0:1;
then A34:
~ a9 >= ~ b9
by YELLOW_7:1;
A35:
~ b9 = b
by LATTICE3:def 7;
~ a9 = A
by LATTICE3:def 7;
then A36:
b c= A
by A34, A35, YELLOW_1:3;
S1[
b,
f . b]
by A9, A12, A35;
then
(R *' f) . b in b
by A27;
hence
A meets V
by A33, A36, XBOOLE_0:3;
verum end;
A is
closed
by A3, A28;
then
Cl A = A
by PRE_TOPC:22;
hence
x in X
by A29, PRE_TOPC:def 7;
verum end; hence
meet F <> {}
by A11, SETFAM_1:def 1;
verum end;
hence
T is compact
by COMPTS_1:4; verum