let S be non empty set ; :: thesis: for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for t being Element of Inf_seq S
for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= 'X' f iff Shift (t,1) |= f )
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); :: thesis: for t being Element of Inf_seq S
for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= 'X' f iff Shift (t,1) |= f )
let t be Element of Inf_seq S; :: thesis: for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= 'X' f iff Shift (t,1) |= f )
let f be Assign of (Inf_seqModel (S,BASSIGN)); :: thesis: ( t |= 'X' f iff Shift (t,1) |= f )
set S1 = Inf_seq S;
set t1 = Shift (t,1);
set t1p = Shift (t,1,S);
A1: 'X' f = Next_0 (f,S) by Def48;
thus ( t |= 'X' f implies Shift (t,1) |= f ) :: thesis: ( Shift (t,1) |= f implies t |= 'X' f )

proof

assume t |= 'X' f ; :: thesis: Shift (t,1) |= f
then (Fid ((Next_0 (f,S)),(Inf_seq S))) . t = TRUE by A1;
then Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE by Def47;
then (Fid (f,(Inf_seq S))) . (Shift (t,1,S)) = TRUE by Def46;
hence Shift (t,1) |= f ; :: thesis: verum

end;

assume Shift (t,1) |= f ; :: thesis: t |= 'X' f
then (Fid (f,(Inf_seq S))) . (Shift (t,1)) = TRUE ;
then Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE by Def46;
then (Fid (('X' f),(Inf_seq S))) . t = TRUE by A1, Def47;
hence t |= 'X' f ; :: thesis: verum