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 A2: 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 set ; :: 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 ;
A3: G is centered

proof

consider A0 being Element of F;
reconsider A0 = A0 as Subset of T by WAYBEL_7:4;
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 A4: ( H <> {} & H c= G & H is finite ) ; :: thesis: not meet H = {}
then reconsider H1 = H as finite Subset-Family of the carrier of T by XBOOLE_1:1;
H1 c= F

proof

let x be set ; :: 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
A5: ( x = Cl A & A in F ) ;
A c= Cl A by PRE_TOPC:48;
hence x in F by A5, WAYBEL_7:11; :: thesis: verum

end;

then Intersect H1 in F by WAYBEL_7:15;
then Intersect H1 <> {} by Th2;
hence not meet H = {} by A4, SETFAM_1:def 10; :: thesis: verum

end;

consider x being 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 A6: meet G <> {} by A2, A3, COMPTS_1:13;
then x in meet G ;
then reconsider x = x 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 A7: ( A is open & x in A ) ; :: thesis: A in F
A8: F is prime by WAYBEL_7:26;
set B = A ` ;

now

assume A ` in F ; :: thesis: contradiction
then ( Cl (A ` ) in G & A ` is closed ) by A7;
then ( A ` in G & not x in A ` ) by A7, PRE_TOPC:52, XBOOLE_0:def 5;
hence contradiction by A6, SETFAM_1:def 1; :: thesis: verum

end;

hence A in F by A8, WAYBEL_7:25; :: thesis: verum

end;

end;

assume A9: 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

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

now

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
A11: ( x <= Bottom (BoolePoset the carrier of T) & x in fininfs Y ) by WAYBEL_0:def 16;
A12: Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
consider Z being finite Subset of Y such that
A13: ( x = "/\" Z,(BoolePoset the carrier of T) & ex_inf_of Z, BoolePoset the carrier of T ) by A11;
reconsider Z = Z as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;
A14: x = Bottom (BoolePoset the carrier of T) by A11, YELLOW_5:22;
then x <> Top (BoolePoset the carrier of T) by WAYBEL_7:5;
then A15: Z <> {} by A13, YELLOW_0:def 12;
then meet Z <> {} by A10, FINSET_1:def 3;
hence contradiction by A12, A13, A14, A15, YELLOW_1:20; :: thesis: verum

end;

then uparrow (fininfs Y) is proper by WAYBEL_7:8;
then consider UF being Filter of (BoolePoset the carrier of T) such that
A16: ( uparrow (fininfs Y) c= UF & UF is ultra ) by WAYBEL_7:30;
consider x being Point of T such that
A17: x is_a_convergence_point_of UF,T by A9, A16;
A18: F <> {} by A10, FINSET_1:def 3;
F c= uparrow (fininfs Y) by WAYBEL_0:62;
then A19: F c= UF by A16, XBOOLE_1:1;

now

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

A21: now

let C be Subset of T; :: thesis: ( C is open & x in C implies A meets C )
assume ( C is open & x in C ) ; :: thesis: A meets C
then A22: ( C in UF & A in UF ) by A17, A19, A20, WAYBEL_7:def 5;
then reconsider c = C, a = A as Element of (BoolePoset the carrier of T) ;
( a "/\" c in UF & UF is ultra Filter of (BoolePoset the carrier of T) ) by A16, A22, WAYBEL_0:41;
then a "/\" c <> {} by Th2;
then A /\ C <> {} by YELLOW_1:17;
hence A meets C by XBOOLE_0:def 7; :: thesis: verum

end;

B is closed by A10, A20, TOPS_2:def 2;
then Cl B = B by PRE_TOPC:52;
hence x in A by A21, PRE_TOPC:54; :: thesis: verum

end;

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

end;

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