( not [#] T is empty & [#] T is finite-ind ) by Def4;
hence ind T is natural ; :: thesis: verum