let A be Subset of T; :: 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 ;
[#] (T | B) = B by PRE_TOPC:def 5;
then A1: T | B is compact ;
( B = {} or B <> {} ) ;
hence A is compact by A1, Th3; :: thesis: verum