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

assume A1: T is compact ; :: thesis:
let N be net of T; :: thesis:
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:
consider x being Point of T such that
A3: x is_a_cluster_point_of N by A1, Lm1;

let V be a_neighborhood of x; :: thesis:
assume not N is_eventually_in V ; :: thesis:
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:

end;

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

end;

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

let F be ultra Filter of (BoolePoset ([#] T)); :: thesis:
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:
thus x is_a_convergence_point_of F,T by A8, Th17; :: thesis:

end;

hence T is compact by Th31; :: thesis: