theorem :: BCIALG_3:48

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