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 )

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

( 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 A2:
X is BCK-algebra of m,n,i,j
; :: thesis: X is BCK-algebra of i,j,m,n
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;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

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