theorem :: BCIALG_1:5

for X being BCI-algebra
for x, y, z being Element of X st x <= y holds
( x \ z <= y \ z & z \ y <= z \ x ) by Th4;