theorem Th60: :: MODELC_2:60

for S being non empty set
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 ) )