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