let v be LTL-formula; :: thesis: for N2, N1 being strict LTLnode of v st N2 is_succ_of N1 holds
len N2 <= (len N1) - 1
let N2, N1 be strict LTLnode of v; :: thesis: ( N2 is_succ_of N1 implies len N2 <= (len N1) - 1 )
set r1 = len the LTLnew of N1;
set r2 = len the LTLnew of N2;
assume N2 is_succ_of N1 ; :: thesis: len N2 <= (len N1) - 1
then ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) by Def9;
then len the LTLnew of N2 <= (len the LTLnew of N1) - 1 by Th19, Th20;
hence len N2 <= (len N1) - 1 by Lm5; :: thesis: verum