theorem :: BCIIDEAL:23

for X being BCK-algebra holds BCK-part X is commutative Ideal of X