:: deftheorem Def10 defines Commutative-Ideal BCIALG_3:def 10 :
for X being BCK-algebra
for b₂ being non empty Subset of X holds
( b₂ is Commutative-Ideal of X iff ( 0. X in b₂ & ( for x, y, z being Element of X st (x \ y) \ z in b₂ & z in b₂ holds
x \ (y \ (y \ x)) in b₂ ) ) );