let T be non empty TopSpace; :: thesis:
set X = the carrier of T;

hereby :: thesis:

assume A1: T is compact ; :: thesis:
let F be ultra Filter of (BoolePoset ([#] T)); :: thesis:
set G = { (Cl A) where A is Subset of T : A in F } ;
{ (Cl A) where A is Subset of T : A in F } c= bool the carrier of T

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (Cl A) where A is Subset of T : A in F } ; :: thesis:
then ex A being Subset of T st
( x = Cl A & A in F ) ;
hence x in bool the carrier of T ; :: thesis:

end;

then reconsider G = { (Cl A) where A is Subset of T : A in F } as Subset-Family of T ;
A2: G is centered

set A0 = the Element of F;
reconsider A0 = the Element of F as Subset of T by WAYBEL_7:2;
Cl A0 in G ;
hence G <> {} ; :: according to FINSET_1:def 3 :: thesis:
let H be set ; :: thesis:
assume that
A3: H <> {} and
A4: H c= G and
A5: H is finite ; :: thesis:
reconsider H1 = H as finite Subset-Family of the carrier of T by A4, A5, XBOOLE_1:1;
H1 c= F

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in H1 ; :: thesis:
then x in G by A4;
then consider A being Subset of T such that
A6: x = Cl A and
A7: A in F ;
A c= Cl A by PRE_TOPC:18;
hence x in F by A6, A7, WAYBEL_7:7; :: thesis:

end;

then Intersect H1 in F by WAYBEL_7:11;
then Intersect H1 <> {} by Th1;
hence not meet H = {} by A3, SETFAM_1:def 9; :: thesis:

end;

set x = the Element of meet G;
G is closed

let A be Subset of T; :: according to TOPS_2:def 2 :: thesis:
assume A in G ; :: thesis:
then ex B being Subset of T st
( A = Cl B & B in F ) ;
hence A is closed ; :: thesis:

end;

then A8: meet G <> {} by A1, A2, COMPTS_1:4;
then the Element of meet G in meet G ;
then reconsider x = the Element of meet G as Point of T ;
take x = x; :: thesis:
thus x is_a_convergence_point_of F,T :: thesis:

let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis:
assume that
A9: A is open and
A10: x in A ; :: thesis:
set B = A ` ;

A11: now :: thesis:

assume A ` in F ; :: thesis:
then Cl (A `) in G ;
then A12: A ` in G by A9, PRE_TOPC:22;
not x in A ` by A10, XBOOLE_0:def 5;
hence contradiction by A8, A12, SETFAM_1:def 1; :: thesis:

end;

F is prime by WAYBEL_7:22;
hence A in F by A11, WAYBEL_7:21; :: thesis:

end;

end;

assume A13: for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ; :: thesis:

set L = BoolePoset the carrier of T;
let F be Subset-Family of T; :: thesis:
assume A14: ( F is centered & F is closed ) ; :: thesis:
reconsider Y = F as Subset of (BoolePoset the carrier of T) by WAYBEL_7:2;
set G = uparrow (fininfs Y);

assume Bottom (BoolePoset the carrier of T) in uparrow (fininfs Y) ; :: thesis:
then consider x being Element of (BoolePoset the carrier of T) such that
A15: x <= Bottom (BoolePoset the carrier of T) and
A16: x in fininfs Y by WAYBEL_0:def 16;
A17: Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
consider Z being finite Subset of Y such that
A18: x = "/\" (Z,(BoolePoset the carrier of T)) and
ex_inf_of Z, BoolePoset the carrier of T by A16;
reconsider Z = Z as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;
A19: x = Bottom (BoolePoset the carrier of T) by A15, YELLOW_5:19;
then x <> Top (BoolePoset the carrier of T) by WAYBEL_7:3;
then A20: Z <> {} by A18, YELLOW_0:def 12;
then meet Z <> {} by A14;
hence contradiction by A17, A18, A19, A20, YELLOW_1:20; :: thesis:

end;

then uparrow (fininfs Y) is proper ;
then consider UF being Filter of (BoolePoset the carrier of T) such that
A21: uparrow (fininfs Y) c= UF and
A22: UF is ultra by WAYBEL_7:26;
consider x being Point of T such that
A23: x is_a_convergence_point_of UF,T by A13, A22;
F c= uparrow (fininfs Y) by WAYBEL_0:62;
then A24: F c= UF by A21;

A25: now :: thesis:

let A be set ; :: thesis:
assume A26: A in F ; :: thesis:
then reconsider B = A as Subset of T ;

A27: now :: thesis:

let C be Subset of T; :: thesis:
assume that
A28: C is open and
A29: x in C ; :: thesis:
A30: C in UF by A23, A28, A29;
A in UF by A24, A26;
then reconsider c = C, a = A as Element of (BoolePoset the carrier of T) by A30;
a "/\" c in UF by A24, A26, A30, WAYBEL_0:41;
then a "/\" c <> {} by A22, Th1;
then A /\ C <> {} by YELLOW_1:17;
hence A meets C ; :: thesis:

end;

B is closed by A14, A26;
then Cl B = B by PRE_TOPC:22;
hence x in A by A27, PRE_TOPC:24; :: thesis:

end;

F <> {} by A14;
hence meet F <> {} by A25, SETFAM_1:def 1; :: thesis:

end;

hence T is compact by COMPTS_1:4; :: thesis: