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