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