theorem Th23: :: MODELC_3:23

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