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 B1: ( H in W & 'not' H in W ) ; :: thesis: r |/= W

now

assume r |= W ; :: thesis: contradiction
then ( r |= H & r |= 'not' H ) by B1, Def66;
hence contradiction by Th19; :: thesis: verum

end;

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