let X be BCI-algebra; :: thesis: ( ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) implies for x, y being Element of X holds (x ` ) \ y = (x \ y) ` )
assume A1: for x, y being Element of X holds (x \ y) ` = (y \ x) ` ; :: 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) `
thus (x \ y) ` = (x ` ) \ (y ` ) by Th9
.= ((y ` ) ` ) \ x by Th7
.= ((y \ (0. X)) ` ) \ x by A1
.= (y ` ) \ x by Th2
.= (x ` ) \ y by Th7 ; :: thesis: verum