theorem :: MODELC_2:73

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