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

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 ` by WAYBEL_0:def 11;
N is_often_in V by A3, WAYBEL_9:def 9;
then consider j being Element of N such that
A5: ( i <= j & N . j in V ) by WAYBEL_0:def 12;
N . j in V ` by A4, A5;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

then x in Lim N by YELLOW_6:def 18;
hence N is convergent by YELLOW_6:def 19; :: thesis: verum

end;

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

now

let F be ultra Filter of (BoolePoset ([#] T)); :: thesis: ex x being Point of T st x is_a_convergence_point_of F,T
consider x being Element of Lim (a_net F);
a_net F is convergent by A6;
then A7: Lim (a_net F) <> {} by YELLOW_6:def 19;
then x in Lim (a_net F) ;
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 by A7, Th18; :: thesis: verum

end;

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