let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'U' H2 iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) )
let r be Element of Inf_seq AtomicFamily; :: thesis: ( r |= H1 'U' H2 iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) )
A1: ( ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) ) & Shift (r,m) |= Evaluate (H2,AtomicKai) ) implies ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) )

proof

assume ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) ) & Shift (r,m) |= Evaluate (H2,AtomicKai) ) ; :: thesis: ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 )
then consider m being Nat such that
A2: for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) and
A3: Shift (r,m) |= Evaluate (H2,AtomicKai) ;
take m ; :: thesis: ( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 )
for j being Nat st j < m holds
Shift (r,j) |= H1 by A2;
hence ( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) by A3; :: thesis: verum

end;

A4: ( ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) implies ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) ) & Shift (r,m) |= Evaluate (H2,AtomicKai) ) )

proof

assume ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) ; :: thesis: ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) ) & Shift (r,m) |= Evaluate (H2,AtomicKai) )
then consider m being Nat such that
A5: for j being Nat st j < m holds
Shift (r,j) |= H1 and
A6: Shift (r,m) |= H2 ;
take m ; :: thesis: ( ( for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) ) & Shift (r,m) |= Evaluate (H2,AtomicKai) )
for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) by A5, Def63;
hence ( ( for j being Nat st j < m holds
Shift (r,j) |= Evaluate (H1,AtomicKai) ) & Shift (r,m) |= Evaluate (H2,AtomicKai) ) by A6; :: thesis: verum

end;

( r |= H1 'U' H2 iff r |= (Evaluate (H1,AtomicKai)) 'U' (Evaluate (H2,AtomicKai)) ) by Th54;
hence ( r |= H1 'U' H2 iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 ) ) by A1, A4, Th60; :: thesis: verum