let i, j, m, n be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n st i = n holds
X is BCK-algebra of i,j,j,i
let X be BCK-algebra of i,j,m,n; :: thesis: ( i = n implies X is BCK-algebra of i,j,j,i )
assume i = n ; :: thesis: X is BCK-algebra of i,j,j,i
then reconsider X = X as BCK-algebra of i,j,m,i ;
for x, y being Element of X holds Polynom i,j,x,y = Polynom j,i,y,x

proof

let x, y be Element of X; :: thesis: Polynom i,j,x,y = Polynom j,i,y,x
Polynom i,j,x,y = Polynom m,i,y,x by Def3;
hence Polynom i,j,x,y = Polynom j,i,y,x by Th20; :: thesis: verum

end;

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