theorem :: BCIALG_5:58

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