theorem Th33: :: MODELC_3:33

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