let X be BCI-algebra; :: thesis: ( ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) implies for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )

assume A1: for x, y being Element of X holds (x `) \ y = (x \ y) ` ; :: thesis: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X

let x, y be Element of X; :: thesis: (x \ y) \ (y \ x) in BCK-part X

((x \ y) \ (y \ x)) ` = ((x \ y) `) \ (y \ x) by A1

.= ((x `) \ (y `)) \ (y \ x) by Th9

.= (((y `) `) \ x) \ (y \ x) by Th7

.= (((y `) \ x) `) \ (y \ x) by A1

.= (((y \ x) `) `) \ (y \ x) by A1

.= 0. X by Th1 ;

then 0. X <= (x \ y) \ (y \ x) ;

hence (x \ y) \ (y \ x) in BCK-part X ; :: thesis: verum

assume A1: for x, y being Element of X holds (x `) \ y = (x \ y) ` ; :: thesis: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X

let x, y be Element of X; :: thesis: (x \ y) \ (y \ x) in BCK-part X

((x \ y) \ (y \ x)) ` = ((x \ y) `) \ (y \ x) by A1

.= ((x `) \ (y `)) \ (y \ x) by Th9

.= (((y `) `) \ x) \ (y \ x) by Th7

.= (((y `) \ x) `) \ (y \ x) by A1

.= (((y \ x) `) `) \ (y \ x) by A1

.= 0. X by Th1 ;

then 0. X <= (x \ y) \ (y \ x) ;

hence (x \ y) \ (y \ x) in BCK-part X ; :: thesis: verum