let T be TopSpace; :: thesis: ( T is finite implies T is compact )
assume T is finite ; :: thesis: T is compact
then the carrier of T is finite ;
hence T is compact by COMPTS_1:27; :: thesis: verum