let T be non empty TopSpace; :: thesis: ( T is compact iff for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T )
set X = the carrier of T;

hereby :: thesis: ( ( for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ) implies T is compact )

assume A1: T is compact ; :: thesis: for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T
let F be ultra Filter of (BoolePoset ([#] T)); :: thesis: ex x being Point of T st x is_a_convergence_point_of F,T
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

proof

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

end;

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

proof

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: for b₁ being set holds
( b₁ = {} or not b₁ c= G or not b₁ is finite or not meet b₁ = {} )
let H be set ; :: thesis: ( H = {} or not H c= G or not H is finite or not meet H = {} )
assume that
A3: H <> {} and
A4: H c= G and
A5: H is finite ; :: thesis: not meet H = {}
reconsider H1 = H as finite Subset-Family of the carrier of T by A4, A5, XBOOLE_1:1;
H1 c= F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1 or x in F )
assume x in H1 ; :: thesis: x in F
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: verum

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: verum

end;

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

proof

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

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: x is_a_convergence_point_of F,T
thus x is_a_convergence_point_of F,T :: thesis: verum

proof

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

A11: now :: thesis: not A ` in F

assume A ` in F ; :: thesis: contradiction
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: verum

end;

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

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: T is compact

now :: thesis: for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {}

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

now :: thesis: not Bottom (BoolePoset the carrier of T) in uparrow (fininfs Y)

assume Bottom (BoolePoset the carrier of T) in uparrow (fininfs Y) ; :: thesis: contradiction
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: verum

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

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

A27: now :: thesis: for C being Subset of T st C is open & x in C holds
A meets C

let C be Subset of T; :: thesis: ( C is open & x in C implies A meets C )
assume that
A28: C is open and
A29: x in C ; :: thesis: A meets C
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: verum

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: verum

end;

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

end;

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