:: deftheorem Def47 defines Next_0 MODELC_2:def 47 :
for S being non empty set
for f being object
for b₃ being Element of ModelSP (Inf_seq S) holds
( b₃ = Next_0 (f,S) iff for t being set st t in Inf_seq S holds
( Next_univ (t,(Fid (f,(Inf_seq S)))) = TRUE iff (Fid (b₃,(Inf_seq S))) . t = TRUE ) );