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

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