let i, j, m, n be Element of 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