theorem :: BCIALG_3:14

for X being commutative BCK-algebra holds
( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra )