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 being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )