theorem :: MODELC_3:42

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