theorem Th20: :: MODELC_3:20

for v being LTL-formula
for N1, N2 being strict LTLnode over v st N2 is_succ2_of N1 holds
len the LTLnew of N2 <= (len the LTLnew of N1) - 1