let X be BCI-Algebra_with_Condition(S); :: thesis: for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)
let x, y, z be Element of X; :: thesis: (x \ y) \ z = x \ (y * z)
(x \ ((x \ y) \ z)) \ y = (x \ y) \ ((x \ y) \ z) by BCIALG_1:7
.= ((x \ y) \ (0. X)) \ ((x \ y) \ z) by BCIALG_1:2 ;
then ((x \ ((x \ y) \ z)) \ y) \ (z \ (0. X)) = 0. X by BCIALG_1:11;
then (x \ ((x \ y) \ z)) \ y <= z \ (0. X) ;
then (x \ ((x \ y) \ z)) \ y <= z by BCIALG_1:2;
then x \ ((x \ y) \ z) <= y * z by Lm2;
then (x \ ((x \ y) \ z)) \ (y * z) = 0. X ;
then A1: (x \ (y * z)) \ ((x \ y) \ z) = 0. X by BCIALG_1:7;
(y * z) \ y <= z by Lm2;
then ( ((x \ y) \ (x \ (y * z))) \ ((y * z) \ y) = 0. X & ((y * z) \ y) \ z = 0. X ) by BCIALG_1:11;
then ((x \ y) \ (x \ (y * z))) \ z = 0. X by BCIALG_1:3;
then ((x \ y) \ z) \ (x \ (y * z)) = 0. X by BCIALG_1:7;
hence (x \ y) \ z = x \ (y * z) by A1, BCIALG_1:def 7; :: thesis: verum