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 |= '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 ) ; :: thesis: verum