let X be BCI-algebra; :: thesis: 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)
let x, y be Element of X; :: thesis: for n being Nat holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y)
let n be Nat; :: thesis: Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y)
(y \ x) \ (y \ x) = 0. X by BCIALG_1:def 5;
then (y \ (y \ x)) \ x = 0. X by BCIALG_1:7;
then y \ (y \ x) <= x ;
then ((y \ (y \ x)),(x \ y)) to_power (n + 1) <= (x,(x \ y)) to_power (n + 1) by BCIALG_2:19;
then ((((y \ (y \ x)),(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:19;
then ((((y \ (y \ x)),(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:11;
then (((((y,(y \ x)) to_power 1),(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:2;
hence Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y) by BCIALG_2:10; :: thesis: verum