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

proof

let x, y be Element of X; :: thesis: Polynom i,j,x,y <= Polynom i,j,y,x
i + 1 <= m + 1 by A1, XREAL_1:8;
then A4: (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 & (y,(y \ x) to_power (i + 1)),(x \ y) to_power n <= (y,(y \ x) to_power (i + 1)),(x \ y) to_power j ) by A2, Def3, Th5;
hence Polynom i,j,x,y <= Polynom i,j,y,x by A4, Th1; :: thesis: verum

end;

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

proof

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

end;

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