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 Th22;
then ( r |= 'X' ('not' H) iff Shift r,1 |/= H ) by Th19;
then ( r |= 'X' ('not' H) iff not r |= 'X' H ) by Th22;
hence ( r |= 'X' ('not' H) iff r |= 'not' ('X' H) ) by Th19; :: thesis: verum