for T being non empty TopSpace holds
( T is compact iff 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 ) by Lm1, Lm2;