theorem Th45: :: BCIALG_4:46

for X being BCK-Algebra_with_Condition(S) holds
( X is positive-implicative iff for x, y being Element of X st x <= y holds
x * y = y )