let X be BCI-algebra; :: thesis: for y, x being Element of X
for n being Element of NAT holds Polynom (n + 1),(n + 1),y,x <= Polynom n,(n + 1),x,y
let y, x be Element of X; :: thesis: for n being Element of NAT holds Polynom (n + 1),(n + 1),y,x <= Polynom n,(n + 1),x,y
let n be Element of 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 by BCIALG_1:def 11;
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