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