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