theorem :: YELLOW19:36

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