for H1, H2 being LTL-formula
for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'R' H2 iff for m being Nat st ( for j being Nat st j < m holds
Shift (r,j) |= 'not' H1 ) holds
Shift (r,m) |= H2 )