for n being Nat holds (Seq_of_ind T) . n c= (Seq_of_ind T) . (n + 1) by Def1;
hence Seq_of_ind T is non-descending by KURATO_0:def 4; :: thesis: verum