for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula
for U being Choice_Function of (BOOL (Subformulae v))
for s being strict elementary LTLnode over v st w |= * ('X' s) holds
( chosen_next (w,v,U,s) is_next_of s & w |= * (chosen_next (w,v,U,s)) )