:: deftheorem Def9 defines commutative BCIALG_4:def 9 :
for IT being BCK-Algebra_with_Condition(S) holds
( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );