let X be 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) )
let a be Element of X; ( a is being_greatest implies ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) )
assume A1:
a is being_greatest
; ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
thus
( X is BCK-implicative implies for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
( ( for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) implies X is BCK-implicative )
assume A5:
for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z)
; X is BCK-implicative
for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X
hence
X is BCK-implicative
by A1, Th43; verum