let H be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= 'X' H iff Shift r,1 |= H )
let r be Element of Inf_seq AtomicFamily ; :: thesis: ( r |= 'X' H iff Shift r,1 |= H )
( r |= 'X' H iff r |= Evaluate ('X' H),AtomicKai ) by Def65;
then ( r |= 'X' H iff r |= 'X' (Evaluate H,AtomicKai ) ) by Th53;
then ( r |= 'X' H iff Shift r,1 |= Evaluate H,AtomicKai ) by Th59;
hence ( r |= 'X' H iff Shift r,1 |= H ) by Def65; :: thesis: verum