let A be Subset of ; :: thesis: ( A is finite implies A is compact )
assume A is finite ; :: thesis: A is compact
then reconsider B = A as finite Subset of ;
[#] (T | B) = B by PRE_TOPC:def 10;
then A1: T | B is compact by Th27;
( B = {} or B <> {} ) ;
hence A is compact by A1, Th12; :: thesis: verum