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