:: deftheorem Def3 defines BCI-algebra BCIALG_5:def 3 :
for i, j, m, n being Nat
for b₅ being BCI-algebra holds
( b₅ is BCI-algebra of i,j,m,n iff for x, y being Element of b₅ holds Polynom (i,j,x,y) = Polynom (m,n,y,x) );