for i, j, k, l, m, n being Nat
for X being BCK-algebra of i,j,m,n st l >= j & k >= n holds
X is BCK-algebra of k,l,l,k