for r being Element of Inf_seq AtomicFamily
for W being Subset of LTL_WFF holds
( r |= 'X' W iff Shift (r,1) |= W )