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