theorem :: BCIALG_5:34

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