let T be non empty TopSpace; :: thesis: ( T is compact iff for N being net of T st N is Cauchy holds
N is convergent )
thus ( T is compact implies for N being net of T st N is Cauchy holds
N is convergent ) :: thesis: ( ( for N being net of T st N is Cauchy holds
N is convergent ) implies T is compact )

proof

assume A1: T is compact ; :: thesis: for N being net of T st N is Cauchy holds
N is convergent
let N be net of T; :: thesis: ( N is Cauchy implies N is convergent )
assume A2: for A being Subset of T holds
( N is_eventually_in A or N is_eventually_in A ` ) ; :: according to YELLOW19:def 5 :: thesis: N is convergent
consider x being Point of T such that
A3: x is_a_cluster_point_of N by A1, Lm1;

now :: thesis: for V being a_neighborhood of x holds N is_eventually_in V

let V be a_neighborhood of x; :: thesis: N is_eventually_in V
assume not N is_eventually_in V ; :: thesis: contradiction
then N is_eventually_in V ` by A2;
then consider i being Element of N such that
A4: for j being Element of N st i <= j holds
N . j in V ` ;
N is_often_in V by A3;
then consider j being Element of N such that
A5: i <= j and
A6: N . j in V ;
N . j in V ` by A4, A5;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum

end;

then x in Lim N by YELLOW_6:def 15;
hence N is convergent by YELLOW_6:def 16; :: thesis: verum

end;

assume A7: for N being net of T st N is Cauchy holds
N is convergent ; :: thesis: T is compact

now :: 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 x = the Element of Lim (a_net F);
a_net F is convergent by A7;
then A8: Lim (a_net F) <> {} by YELLOW_6:def 16;
then the Element of Lim (a_net F) in Lim (a_net F) ;
then reconsider x = the Element of Lim (a_net F) 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 by A8, Th17; :: thesis: verum

end;

hence T is compact by Th31; :: thesis: verum