theorem :: BCIALG_3:15

for X being BCK-algebra st X is BCI-weakly-commutative BCI-algebra holds
X is BCI-commutative