let X be BCI-algebra; :: thesis: for i, j, m, n being Nat holds
( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )
let i, j, m, n be Nat; :: thesis: ( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )
thus ( X is BCK-algebra of i,j,m,n implies X is BCK-algebra of m,n,i,j ) :: thesis: ( X is BCK-algebra of m,n,i,j implies X is BCK-algebra of i,j,m,n )

proof

assume A1: X is BCK-algebra of i,j,m,n ; :: thesis: X is BCK-algebra of m,n,i,j
then for x, y being Element of X holds Polynom (m,n,x,y) = Polynom (i,j,y,x) by Def3;
hence X is BCK-algebra of m,n,i,j by A1, Def3; :: thesis: verum

end;

assume A2: X is BCK-algebra of m,n,i,j ; :: thesis: X is BCK-algebra of i,j,m,n
then for x, y being Element of X holds Polynom (m,n,y,x) = Polynom (i,j,x,y) by Def3;
hence X is BCK-algebra of i,j,m,n by A2, Def3; :: thesis: verum