let X be BCI-algebra; :: thesis: for x, y being Element of X holds (x \ y) ` = (x ` ) \ (y ` )
let x, y be Element of X; :: thesis: (x \ y) ` = (x ` ) \ (y ` )
(x ` ) \ (y ` ) = (((x \ y) \ (x \ y)) \ x) \ (y ` ) by Def5
.= (((x \ y) \ x) \ (x \ y)) \ (y ` ) by Th7
.= (((x \ x) \ y) \ (x \ y)) \ (y ` ) by Th7
.= ((y ` ) \ (x \ y)) \ (y ` ) by Def5
.= ((y ` ) \ (y ` )) \ (x \ y) by Th7 ;
hence (x \ y) ` = (x ` ) \ (y ` ) by Def5; :: thesis: verum