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

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 :: thesis: for F being Subset-Family of T st F is centered & F is closed holds

meet F <> {}

hence
T is compact
by COMPTS_1:4; :: thesis: verummeet F <> {}

set X = the carrier of T;

defpred S_{1}[ object , object ] means ex A being set st

( A = $1 & $2 in A );

let F be Subset-Family of T; :: thesis: ( F is centered & F is closed implies meet F <> {} )

assume that

A2: F is centered and

A3: F is closed ; :: thesis: meet F <> {}

set G = FinMeetCl F;

A8: ( dom f = FinMeetCl F & rng f c= the carrier of T ) and

A9: for a being object st a in FinMeetCl F holds

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

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;

end;defpred S

( A = $1 & $2 in A );

let F be Subset-Family of T; :: thesis: ( F is centered & F is closed implies meet F <> {} )

assume that

A2: F is centered and

A3: F is closed ; :: thesis: meet F <> {}

set G = FinMeetCl F;

A4: now :: thesis: for x being object st x in FinMeetCl F holds

ex y being object st

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

consider f being Function such that ex y being object st

( y in the carrier of T & S

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

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

reconsider xx = x as set by TARSKI:1;

set y = the Element of xx;

assume x in FinMeetCl F ; :: thesis: ex y being object st

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

then consider Y being Subset-Family of T such that

A5: Y c= F and

A6: Y is finite and

A7: x = Intersect Y by CANTOR_1:def 3;

( x = the carrier of T or ( x = meet Y & meet Y <> {} ) ) by A2, A5, A6, A7, SETFAM_1:def 9;

then the Element of xx in xx ;

hence ex y being object st

( y in the carrier of T & S_{1}[x,y] )
by A7; :: thesis: verum

end;( y in the carrier of T & S

reconsider xx = x as set by TARSKI:1;

set y = the Element of xx;

assume x in FinMeetCl F ; :: thesis: ex y being object st

( y in the carrier of T & S

then consider Y being Subset-Family of T such that

A5: Y c= F and

A6: Y is finite and

A7: x = Intersect Y by CANTOR_1:def 3;

( x = the carrier of T or ( x = meet Y & meet Y <> {} ) ) by A2, A5, A6, A7, SETFAM_1:def 9;

then the Element of xx in xx ;

hence ex y being object st

( y in the carrier of T & S

A8: ( dom f = FinMeetCl F & rng f c= the carrier of T ) and

A9: for a being object st a in FinMeetCl F holds

S

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

then reconsider R = (InclPoset G) opp as non empty transitive directed RelStr ;
let x, y be Element of ((InclPoset G) opp); :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] ((InclPoset G) opp) or not y in [#] ((InclPoset G) opp) or ex b_{1} being Element of the carrier of ((InclPoset G) opp) st

( b_{1} in [#] ((InclPoset G) opp) & x <= b_{1} & y <= b_{1} ) )

assume that

x in [#] ((InclPoset G) opp) and

y in [#] ((InclPoset G) opp) ; :: thesis: ex b_{1} being Element of the carrier of ((InclPoset G) opp) st

( b_{1} in [#] ((InclPoset G) opp) & x <= b_{1} & y <= b_{1} )

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 ; :: thesis: ( z in [#] ((InclPoset G) opp) & x <= z & y <= z )

thus z in [#] ((InclPoset G) opp) ; :: thesis: ( 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; :: thesis: verum

end;( b

assume that

x in [#] ((InclPoset G) opp) and

y in [#] ((InclPoset G) opp) ; :: thesis: ex b

( b

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 ; :: thesis: ( z in [#] ((InclPoset G) opp) & x <= z & y <= z )

thus z in [#] ((InclPoset G) opp) ; :: thesis: ( 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; :: thesis: verum

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 :: thesis: for X being set st X in F holds

x in X

hence
meet F <> {}
by A11, SETFAM_1:def 1; :: thesis: verumx in X

let X be set ; :: thesis: ( X in F implies x in X )

assume A28: X in F ; :: thesis: x in X

then reconsider A = X as Subset of T ;

reconsider a = X as Element of (R *' f) by A10, A12, A24, A28, YELLOW_6:3;

then Cl A = A by PRE_TOPC:22;

hence x in X by A29, PRE_TOPC:def 7; :: thesis: verum

end;assume A28: X in F ; :: thesis: x in X

then 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 :: thesis: for V being Subset of T st V is open & x in V holds

A meets V

A is closed
by A3, A28;A meets V

let V be Subset of T; :: thesis: ( V is open & x in V implies A meets V )

assume that

A30: V is open and

A31: x in V ; :: thesis: 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;

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

end;assume that

A30: V is open and

A31: x in V ; :: thesis: 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;

S

then (R *' f) . b in b by A27;

hence A meets V by A33, A36, XBOOLE_0:3; :: thesis: verum

then Cl A = A by PRE_TOPC:22;

hence x in X by A29, PRE_TOPC:def 7; :: thesis: verum