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 (LTLModel 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 (LTLModel 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 (LTLModel 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 (LTLModel 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 V = LTLModel S,BASSIGN;
set S1 = Inf_seq S;
A1: f 'U' g = Until_0 f,g,S by Def54;
A2: ( 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, Def59;
then Until_univ t,(Fid f,(Inf_seq S)),(Fid g,(Inf_seq S)),S = TRUE by Def53;
then consider m being Nat such that
B1: for j being Nat st j < m holds
(Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE and
B2: (Fid g,(Inf_seq S)) . (Shift t,m,S) = TRUE by Def52;
B4: for j being Nat st j < m holds
Shift t,j |= f

proof

let j be Nat; :: thesis: ( j < m implies Shift t,j |= f )
assume C1: j < m ; :: thesis: Shift t,j |= f
set t1 = Shift t,j;
(Fid f,(Inf_seq S)) . (Shift t,j) = TRUE by C1, B1;
hence Shift t,j |= f by Def59; :: thesis: verum

end;

take m ; :: thesis: ( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g )
thus ( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) by B4, Def59, B2; :: thesis: verum

end;

( 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 B1: 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
C1: for j being Nat st j < m holds
Shift t,j |= f and
C2: Shift t,m |= g by B1;
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 D1: j < m ; :: thesis: (Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE
set t1 = Shift t,j,S;
Shift t,j |= f by D1, C1;
hence (Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE by Def59; :: 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 C2, Def59; :: thesis: verum

end;

then Until_univ t,(Fid f,(Inf_seq S)),(Fid g,(Inf_seq S)),S = TRUE by Def52;
then (Fid (f 'U' g),(Inf_seq S)) . t = TRUE by A1, Def53;
hence t |= f 'U' g by Def59; :: 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