let H be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= 'not' H iff r |/= H )
let r be Element of Inf_seq AtomicFamily; :: thesis: ( r |= 'not' H iff r |/= H )
( r |= 'not' H iff r |= Evaluate (('not' H),AtomicKai) ) by Def67;
then ( r |= 'not' H iff r |= 'not' (Evaluate (H,AtomicKai)) ) by Th50;
then ( r |= 'not' H iff r |/= Evaluate (H,AtomicKai) ) by Th57;
hence ( r |= 'not' H iff r |/= H ) by Def67; :: thesis: verum