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

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