(Seq_of_ind T) . 0 = {({} T)} by Def1;
then {({} T)} is finite-ind ;
hence ex b₁ being Subset-Family of T st
( not b₁ is empty & b₁ is finite-ind ) ; :: thesis: verum