:: deftheorem Def6 defines commutative BCIIDEAL:def 6 :
for X being BCK-algebra
for IT being Ideal of X holds
( IT is commutative iff for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds
x \ (y \ (y \ x)) in IT );