let X be BCI-algebra; :: thesis: for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X
let x, y be Element of X; :: thesis: ((0. X) \ (x \ y)) \ (y \ x) = 0. X
(((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((0. X) \ x) \ (y \ x)) \ ((0. X) \ y) by BCIALG_1:7;
then A1: (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((y \ x) `) \ x) \ ((0. X) \ y) by BCIALG_1:7
.= (((y `) \ (x `)) \ x) \ ((0. X) \ y) by BCIALG_1:9
.= (((y `) \ x) \ (x `)) \ ((0. X) \ y) by BCIALG_1:7
.= (((y `) \ x) \ (y `)) \ (x `) by BCIALG_1:7
.= (((y `) \ (y `)) \ x) \ (x `) by BCIALG_1:7
.= (x `) \ (x `) by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 5 ;
((0. X) \ (x \ y)) \ (y \ x) = ((x \ y) `) \ (y \ x)
.= ((x `) \ (y `)) \ (y \ x) by BCIALG_1:9
.= (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) ;
hence ((0. X) \ (x \ y)) \ (y \ x) = 0. X by A1; :: thesis: verum