let X be BCI-algebra; :: thesis: for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)
let x, y, z, u be Element of X; :: thesis: ( x <= y implies u \ (z \ x) <= u \ (z \ y) )
assume x <= y ; :: thesis: u \ (z \ x) <= u \ (z \ y)
then z \ y <= z \ x by BCIALG_1:5;
hence u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; :: thesis: verum