:: deftheorem Def53 defines EUntill_0 MODELC_1:def 53 :
for S being non empty set
for R being total Relation of S,S
for f, g being set
for b₅ being Element of ModelSP S holds
( b₅ = EUntill_0 (f,g,R) iff for s being set st s in S holds
( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (b₅,S)) . s = TRUE ) );