theorem :: BCIALG_5:16

for X being BCI-algebra
for i, j, m, n being Nat holds
( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )