for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) )