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)
A1: (z * (x * y)) \ z <= x * y by Lm2;
(((x * y) * z) \ x) \ z = (((x * y) * z) \ z) \ x by BCIALG_1:7
.= ((z * (x * y)) \ z) \ x by Th6 ;
then (((x * y) * z) \ x) \ z <= (x * y) \ x by A1, BCIALG_1:5;
then A2: ((((x * y) * z) \ x) \ z) \ ((x * y) \ x) = 0. X ;
A3: (x * (z * y)) \ x <= z * y by Lm2;
(((z * y) * x) \ z) \ x = (((z * y) * x) \ x) \ z by BCIALG_1:7
.= ((x * (z * y)) \ x) \ z by Th6 ;
then (((z * y) * x) \ z) \ x <= (z * y) \ z by A3, BCIALG_1:5;
then A4: ((((z * y) * x) \ z) \ x) \ ((z * y) \ z) = 0. X ;
(z * y) \ z <= y by Lm2;
then ((z * y) \ z) \ y = 0. X ;
then ((((z * y) * x) \ z) \ x) \ y = 0. X by A4, BCIALG_1:3;
then (((z * y) * x) \ z) \ x <= y ;
then ((z * y) * x) \ z <= x * y by Lm2;
then (z * y) * x <= z * (x * y) by Lm2;
then (y * z) * x <= z * (x * y) by Th6;
then x * (y * z) <= z * (x * y) by Th6;
then x * (y * z) <= (x * y) * z by Th6;
then A5: (x * (y * z)) \ ((x * y) * z) = 0. X ;
(x * y) \ x <= y by Lm2;
then ((x * y) \ x) \ y = 0. X ;
then ((((x * y) * z) \ x) \ z) \ y = 0. X by A2, BCIALG_1:3;
then (((x * y) * z) \ x) \ z <= y ;
then ((x * y) * z) \ x <= z * y by Lm2;
then (x * y) * z <= x * (z * y) by Lm2;
then (x * y) * z <= x * (y * z) by Th6;
then ((x * y) * z) \ (x * (y * z)) = 0. X ;
hence (x * y) * z = x * (y * z) by A5, BCIALG_1:def 7; :: thesis: verum