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