len the LTLnew of N >= 0 by Th17;
hence [\(len the LTLnew of N)/] is Nat by INT_1:53; :: thesis: verum