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