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, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) )
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); :: thesis: for t being Element of Inf_seq S
for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) )
let t be Element of Inf_seq S; :: thesis: for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) )
let f, g be Assign of (Inf_seqModel (S,BASSIGN)); :: thesis: ( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) )
set S1 = Inf_seq S;
A1: f 'U' g = Until_0 (f,g,S) by Def53;
A2: ( ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) implies t |= f 'U' g )

proof

assume A3: ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) ; :: thesis: t |= f 'U' g
ex m being Nat st
( ( for j being Nat st j < m holds
(Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE ) & (Fid (g,(Inf_seq S))) . (Shift (t,m,S)) = TRUE )

proof

consider m being Nat such that
A4: for j being Nat st j < m holds
Shift (t,j) |= f and
A5: Shift (t,m) |= g by A3;
take m ; :: thesis: ( ( for j being Nat st j < m holds
(Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE ) & (Fid (g,(Inf_seq S))) . (Shift (t,m,S)) = TRUE )
for j being Nat st j < m holds
(Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE

proof

let j be Nat; :: thesis: ( j < m implies (Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE )
assume j < m ; :: thesis: (Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE
then Shift (t,j) |= f by A4;
hence (Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE ; :: thesis: verum

end;

hence ( ( for j being Nat st j < m holds
(Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE ) & (Fid (g,(Inf_seq S))) . (Shift (t,m,S)) = TRUE ) by A5; :: thesis: verum

end;

then Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE by Def51;
then (Fid ((f 'U' g),(Inf_seq S))) . t = TRUE by A1, Def52;
hence t |= f 'U' g ; :: thesis: verum

end;

( t |= f 'U' g implies ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) )

proof

assume t |= f 'U' g ; :: thesis: ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g )
then (Fid ((Until_0 (f,g,S)),(Inf_seq S))) . t = TRUE by A1;
then Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE by Def52;
then consider m being Nat such that
A6: for j being Nat st j < m holds
(Fid (f,(Inf_seq S))) . (Shift (t,j,S)) = TRUE and
A7: (Fid (g,(Inf_seq S))) . (Shift (t,m,S)) = TRUE by Def51;
take m ; :: thesis: ( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g )
for j being Nat st j < m holds
Shift (t,j) |= f by A6;
hence ( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) by A7; :: thesis: verum

end;

hence ( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (t,j) |= f ) & Shift (t,m) |= g ) ) by A2; :: thesis: verum