:: deftheorem Def55 defines Release_ MODELC_2:def 55 :
for S being non empty set
for b₂ being BinOp of (ModelSP (Inf_seq S)) holds
( b₂ = Release_ S iff for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b₂ . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g))) );