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

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