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

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