theorem :: BCIALG_5:55

for X being BCI-algebra
for m, n being Nat st X is BCI-algebra of n, 0 ,m,m holds
X is BCI-commutative BCI-algebra