let T be TopSpace; :: thesis: ( T is empty implies T is finite-ind )
assume T is empty ; :: thesis: T is finite-ind
then [#] T is finite-ind ;
hence T is finite-ind by Def4; :: thesis: verum