theorem :: COMPTS_1:18

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