theorem Th7: :: BCIALG_1:7
for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y