now

let n be Element of NAT ; :: thesis: (Seq_of_ind T) . n c= (Seq_of_ind T) . (n + 1)
thus (Seq_of_ind T) . n c= (Seq_of_ind T) . (n + 1) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seq_of_ind T) . n or x in (Seq_of_ind T) . (n + 1) )
assume x in (Seq_of_ind T) . n ; :: thesis: x in (Seq_of_ind T) . (n + 1)
hence x in (Seq_of_ind T) . (n + 1) by Def1; :: thesis: verum

end;

end;

hence Seq_of_ind T is non-descending by KURATO_2:def 6; :: thesis: verum