let X be BCI-algebra; :: thesis: 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; :: thesis: for n being Nat holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x)
let n be 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 ;
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