let T be non empty TopSpace; :: thesis: ( T is compact iff for N being net of T ex S being subnet of N st S is convergent )

hereby :: thesis: ( ( for N being net of T ex S being subnet of N st S is convergent ) implies T is compact )

assume A1: T is compact ; :: thesis: for N being net of T ex S being subnet of N st S is convergent
let N be net of T; :: thesis: ex S being subnet of N st S is convergent
consider x being Point of T such that
A2: x is_a_cluster_point_of N by A1, Th33;
consider S being subnet of N such that
A3: x in Lim S by A2, WAYBEL_9:32;
take S = S; :: thesis: S is convergent
thus S is convergent by A3, YELLOW_6:def 16; :: thesis: verum

end;

assume A4: for N being net of T ex S being subnet of N st S is convergent ; :: thesis: T is compact

now :: thesis: for N being net of T ex x being Point of T st x is_a_cluster_point_of N

let N be net of T; :: thesis: ex x being Point of T st x is_a_cluster_point_of N
consider S being subnet of N such that
A5: S is convergent by A4;
set x = the Element of Lim S;
A6: Lim S <> {} by A5, YELLOW_6:def 16;
then the Element of Lim S in Lim S ;
then reconsider x = the Element of Lim S as Point of T ;
take x = x; :: thesis: x is_a_cluster_point_of N
thus x is_a_cluster_point_of N by A6, WAYBEL_9:29, WAYBEL_9:31; :: thesis: verum

end;

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