for H1, H2 being LTL-formula
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 ) )