let H be LTL-formula; :: thesis: 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
let r be Element of Inf_seq AtomicFamily; :: thesis: for W being Subset of LTL_WFF st H in W & 'not' H in W holds
r |/= W
let W be Subset of LTL_WFF; :: thesis: ( H in W & 'not' H in W implies r |/= W )
assume A1: ( H in W & 'not' H in W ) ; :: thesis: r |/= W

now :: thesis: not r |= W

assume r |= W ; :: thesis: contradiction
then ( r |= H & r |= 'not' H ) by A1;
hence contradiction by Th64; :: thesis: verum

end;

hence r |/= W ; :: thesis: verum