:: deftheorem Def16 defines Polish-binOp POLNOT_2:def 12 :
for B being Polish-arity-function
for Z being b₁ -closed Polish-language
for p being FinSequence st p in dom B & B . p = 2 holds
for b₄ being BinOp of Z holds
( b₄ = Polish-binOp (B,Z,p) iff for q, r being FinSequence st q in Z & r in Z holds
b₄ . (q,r) = p ^ (q ^ r) );