for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula
for N being strict LTLnode over v st w |= * N holds
Shift (w,1) |= * ('X' N)