:: deftheorem Def52 defines Until_0 MODELC_2:def 52 :
for S being non empty set
for f, g being set
for b₄ being Element of ModelSP (Inf_seq S) holds
( b₄ = Until_0 (f,g,S) iff for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (b₄,(Inf_seq S))) . t = TRUE ) );