theorem Th9: :: BCIALG_1:9

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