let T be non empty TopSpace; :: thesis: ( T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N )

thus ( T is compact implies for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) by Lm1; :: thesis: ( ( for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) implies T is compact )

assume for N being net of T ex x being Point of T st x is_a_cluster_point_of N ; :: thesis: T is compact

then for N being net of T st N in NetUniv T holds

ex x being Point of T st x is_a_cluster_point_of N ;

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

thus ( T is compact implies for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) by Lm1; :: thesis: ( ( for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) implies T is compact )

assume for N being net of T ex x being Point of T st x is_a_cluster_point_of N ; :: thesis: T is compact

then for N being net of T st N in NetUniv T holds

ex x being Point of T st x is_a_cluster_point_of N ;

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