for T being non empty TopSpace holds
( T is compact iff for N being net of T ex S being subnet of N st S is convergent )