let H be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= 'X' ('not' H) iff r |= 'not' ('X' H) )
let r be Element of Inf_seq AtomicFamily; :: thesis: ( r |= 'X' ('not' H) iff r |= 'not' ('X' H) )
( r |= 'X' ('not' H) iff Shift (r,1) |= 'not' H ) by Th67;
then ( r |= 'X' ('not' H) iff Shift (r,1) |/= H ) by Th64;
then ( r |= 'X' ('not' H) iff not r |= 'X' H ) by Th67;
hence ( r |= 'X' ('not' H) iff r |= 'not' ('X' H) ) by Th64; :: thesis: verum