theorem Th13: :: BCIALG_5:13
for X being BCI-algebra
for i, j, m, n being Nat holds
( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j )