theorem :: BCIIDEAL:3

for X being BCI-algebra
for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u