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

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