theorem Th46: :: BCIALG_4:47

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