theorem Th34: :: MODELC_3:34

for m being Nat
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v holds
the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v))