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
A1: ((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) ;
A5: (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((0. X) \ x) \ (y \ x)) \ ((0. X) \ y) by BCIALG_1:7;
(((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((y \ x) ` ) \ x) \ ((0. X) \ y) by A5, 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 ;
hence ((0. X) \ (x \ y)) \ (y \ x) = 0. X by A1; :: thesis: verum