theorem :: BCIIDEAL:32

for X being BCK-algebra holds the carrier of X is commutative Ideal of X