theorem Th21: :: MODELC_3:21

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