let X be 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)
let x, y be Element of X; for n being Nat holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y)
let n be Nat; 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; verum