let v be LTL-formula; :: thesis: for N being strict LTLnode of v st len N <= 0 holds
the LTLnew of N = {} v
let N be strict LTLnode of v; :: thesis: ( len N <= 0 implies the LTLnew of N = {} v )
A1: (len the LTLnew of N) - 1 < [\(len the LTLnew of N)/] by INT_1:def 4;
assume len N <= 0 ; :: thesis: the LTLnew of N = {} v
then ((len the LTLnew of N) - 1) + 1 < 0 + 1 by A1, XREAL_1:10;
hence the LTLnew of N = {} v by Thlen1201; :: thesis: verum