for v being LTL-formula
for N being strict LTLnode over v
for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of (BOOL (Subformulae v)) st not N is elementary & chosen_formula (U,N) is Until & w |= the_right_argument_of (chosen_formula (U,N)) holds
( ( the_right_argument_of (chosen_formula (U,N)) in the LTLnew of (chosen_succ (w,v,U,N)) or the_right_argument_of (chosen_formula (U,N)) in the LTLold of N ) & chosen_formula (U,N) in the LTLold of (chosen_succ (w,v,U,N)) )