theorem Th5: :: BCIALG_3:5

for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )