theorem :: BCIALG_5:11

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