theorem :: BCIIDEAL:1

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