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