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 w |= * N & not N is elementary holds
( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N )