theorem :: MODELC_3:24

for v being LTL-formula
for N being strict LTLnode over v ex n being Nat ex L being FinSequence ex M being strict LTLnode over v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )