for H being LTL-formula
for r being Element of Inf_seq AtomicFamily holds
( r |= 'X' H iff Shift (r,1) |= H )