:: deftheorem Def51 defines Until_univ MODELC_2:def 51 :
for S being non empty set
for f, g being Function of (Inf_seq S),BOOLEAN
for t being set holds
( ( t is Element of Inf_seq S & ex m being Nat st
( ( for j being Nat st j < m holds
f . (Shift (t,j,S)) = TRUE ) & g . (Shift (t,m,S)) = TRUE ) implies Until_univ (t,f,g,S) = TRUE ) & ( ( not t is Element of Inf_seq S or for m being Nat holds
( ex j being Nat st
( j < m & not f . (Shift (t,j,S)) = TRUE ) or not g . (Shift (t,m,S)) = TRUE ) ) implies Until_univ (t,f,g,S) = FALSE ) );