theorem Th31: :: MODELC_3:31

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