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 Th13;
then x * z <= (y * (x \ y)) * z by Th8;
then x * z <= (y * z) * (x \ y) by Th11;
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 by BCIALG_1:def 11;
((y * z) * (x \ y)) \ (y * z) <= x \ y by Lm2;
then (((y * z) * (x \ y)) \ (y * z)) \ (x \ y) = 0. X by BCIALG_1:def 11;
then ((x * z) \ (y * z)) \ (x \ y) = 0. X by A1, BCIALG_1:3;
hence (x * z) \ (y * z) <= x \ y by BCIALG_1:def 11; :: thesis: verum