theorem Th8: :: BCIALG_1:8

for X being BCI-algebra
for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y