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

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