theorem Th48: :: BCIALG_4:49

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