let A be Subset of TM; :: thesis: ( A is countable implies A is finite-ind )
assume A1: A is countable ; :: thesis: A is finite-ind
TM | A is T_4 ;
hence A is finite-ind by A1, Th19; :: thesis: verum