let X be BCI-algebra; :: thesis: for x, y, z being Element of X st x <= y holds
( x \ z <= y \ z & z \ y <= z \ x )
let x, y, z be Element of X; :: thesis: ( x <= y implies ( x \ z <= y \ z & z \ y <= z \ x ) )
assume x <= y ; :: thesis: ( x \ z <= y \ z & z \ y <= z \ x )
then x \ y = 0. X by Def11;
then ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by Th4;
hence ( x \ z <= y \ z & z \ y <= z \ x ) by Def11; :: thesis: verum