for X being bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )