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 = n & i = m 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 = n & i = m implies X is BCK-algebra of i,i,i,i )
assume A1: i = min (i,j,m,n) ; :: thesis: ( not i = n or not i = m or X is BCK-algebra of i,i,i,i )
assume A2: ( i = n & i = m ) ; :: thesis: X is BCK-algebra of i,i,i,i
then for x, y being Element of X holds Polynom (i,i,x,y) = Polynom (i,j,y,x) by Def3;
then A3: X is BCK-algebra of i,i,i,j by Def3;
i = min (i,i,i,j) by A1, A2;
hence X is BCK-algebra of i,i,i,i by A3, Th27; :: thesis: verum