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 A4:
for N being net of T ex S being subnet of N st S is convergent
; :: thesis: 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;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

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

hence
T is compact
by Th33; :: thesis: verumlet 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;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