theorem Th19: :: MODELC_3:19

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