let v be LTL-formula; :: thesis: for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds
len N2 <= (len N1) - 1
let N1, N2 be strict LTLnode over 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 ) ;
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