theorem Th22: :: MODELC_3:22

for v being LTL-formula
for N being strict LTLnode over v st len N <= 0 holds
the LTLnew of N = {} v