let X be BCI-algebra; :: thesis: for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
let x, y, z, u be Element of X; :: thesis: (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
((x \ (y \ z)) \ (x \ (y \ u))) \ ((y \ u) \ (y \ z)) = 0. X by BCIALG_1:1;
then (x \ (y \ z)) \ (x \ (y \ u)) <= (y \ u) \ (y \ z) ;
then A1: ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= ((y \ u) \ (y \ z)) \ (z \ u) by BCIALG_1:5;
((y \ u) \ (y \ z)) \ (z \ u) = ((y \ u) \ (z \ u)) \ (y \ z) by BCIALG_1:7;
then ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= 0. X by A1, BCIALG_1:def 3;
then (((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u)) \ (0. X) = 0. X ;
then ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) = 0. X by BCIALG_1:2;
hence (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u ; :: thesis: verum