theorem :: BCIALG_5:52

for X being quasi-commutative BCK-algebra holds
( X is BCK-algebra of 0 ,1, 0 ,1 iff for x, y being Element of X holds x \ y = (x \ y) \ y ) by BCIALG_3:28, Th49;