:: deftheorem Def48 defines Next_ MODELC_2:def 48 :
for S being non empty set
for b₂ being UnOp of (ModelSP (Inf_seq S)) holds
( b₂ = Next_ S iff for f being object st f in ModelSP (Inf_seq S) holds
b₂ . f = Next_0 (f,S) );