theorem Th21: :: BCIALG_5:21

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j,j,n