theorem Th47: :: BCIALG_4:48

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