theorem :: BCIALG_5:12

for X being BCI-algebra
for x, y being Element of X
for n being Nat holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x)