let X be BCI-Algebra_with_Condition(S); :: thesis: for x, y, z being Element of X holds (x * z) \ (y * z) <= x \ y
let x, y, z be Element of X; :: thesis: (x * z) \ (y * z) <= x \ y
x <= y * (x \ y) by Th12;
then x * z <= (y * (x \ y)) * z by Th7;
then x * z <= (y * z) * (x \ y) by Th10;
then (x * z) \ (y * z) <= ((y * z) * (x \ y)) \ (y * z) by BCIALG_1:5;
then A1: ((x * z) \ (y * z)) \ (((y * z) * (x \ y)) \ (y * z)) = 0. X ;
((y * z) * (x \ y)) \ (y * z) <= x \ y by Lm2;
then (((y * z) * (x \ y)) \ (y * z)) \ (x \ y) = 0. X ;
then ((x * z) \ (y * z)) \ (x \ y) = 0. X by A1, BCIALG_1:3;
hence (x * z) \ (y * z) <= x \ y ; :: thesis: verum