for H being LTL-formula
for r being Element of Inf_seq AtomicFamily
for W being Subset of LTL_WFF st H in W & 'not' H in W holds
r |/= W