let G be Subset-Family of T; :: thesis: ( G is empty implies G is finite-ind )
assume G is empty ; :: thesis: G is finite-ind
then A1: G c= {({} T)} ;
(Seq_of_ind T) . 0 = {({} T)} by Def1;
hence G is finite-ind by A1; :: thesis: verum