theorem Th37: :: MODELC_3:37

for v being LTL-formula
for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 holds
the LTLnext of s1 c= the LTLold of s2