theorem Th40: :: MODELC_3:40

for H, v being LTL-formula
for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 & H is Release & H in the LTLnext of s1 holds
( the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2 )