for T being TopSpace st the carrier of T is finite holds
T is compact ;