let i, j, m, n be Nat; :: thesis: for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = j holds
X is BCK-algebra of i,i,i,i
let X be BCK-algebra of i,j,m,n; :: thesis: ( i = min (i,j,m,n) & i = j implies X is BCK-algebra of i,i,i,i )
assume A1: i = min (i,j,m,n) ; :: thesis: ( not i = j or X is BCK-algebra of i,i,i,i )
assume A2: i = j ; :: thesis: X is BCK-algebra of i,i,i,i
A3: for x, y being Element of X holds Polynom (i,i,x,y) <= Polynom (i,i,y,x)

proof

let x, y be Element of X; :: thesis: Polynom (i,i,x,y) <= Polynom (i,i,y,x)
i <= n by A1, Th25;
then A4: (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power i by Th5;
i <= m by A1, Th25;
then i + 1 <= m + 1 by XREAL_1:6;
then A5: (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n by Th5, BCIALG_2:19;
Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3;
hence Polynom (i,i,x,y) <= Polynom (i,i,y,x) by A2, A5, A4, Th1; :: thesis: verum

end;

for x, y being Element of X holds Polynom (i,i,y,x) = Polynom (i,i,x,y)

proof

let x, y be Element of X; :: thesis: Polynom (i,i,y,x) = Polynom (i,i,x,y)
Polynom (i,i,x,y) <= Polynom (i,i,y,x) by A3;
then A6: (Polynom (i,i,x,y)) \ (Polynom (i,i,y,x)) = 0. X ;
Polynom (i,i,y,x) <= Polynom (i,i,x,y) by A3;
then (Polynom (i,i,y,x)) \ (Polynom (i,i,x,y)) = 0. X ;
hence Polynom (i,i,y,x) = Polynom (i,i,x,y) by A6, BCIALG_1:def 7; :: thesis: verum

end;

hence X is BCK-algebra of i,i,i,i by Def3; :: thesis: verum