for i, j, k, m, n being Nat
for X being BCK-algebra of i,j,m,n st k >= max (i,j,m,n) holds
X is BCK-algebra of k,k,k,k