:: deftheorem Def54 defines Or_ MODELC_2:def 54 :
for S being non empty set
for b₂ being BinOp of (ModelSP (Inf_seq S)) holds
( b₂ = Or_ 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) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) );