:: deftheorem Def46 defines Next_univ MODELC_2:def 46 :
for S being non empty set
for f being Function of (Inf_seq S),BOOLEAN
for t being set holds
( ( t is Element of Inf_seq S & f . (Shift (t,1,S)) = TRUE implies Next_univ (t,f) = TRUE ) & ( ( not t is Element of Inf_seq S or not f . (Shift (t,1,S)) = TRUE ) implies Next_univ (t,f) = FALSE ) );