let X be BCK-algebra; :: thesis: ( X is BCI-weakly-commutative BCI-algebra implies X is BCI-commutative )
assume A1: X is BCI-weakly-commutative BCI-algebra ; :: thesis: X is BCI-commutative
let x, y be Element of X; :: according to BCIALG_3:def 4 :: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume x \ y = 0. X ; :: thesis: x = y \ (y \ x)
then (x \ (0. X)) \ ((0. X) \ (0. X)) = y \ (y \ x) by A1, Def5;
then (x \ (0. X)) \ (0. X) = y \ (y \ x) by BCIALG_1:def 5;
then x \ (0. X) = y \ (y \ x) by BCIALG_1:2;
hence x = y \ (y \ x) by BCIALG_1:2; :: thesis: verum