for X being BCI-algebra
for x, y, z being Element of X st x <= y & y <= z holds
x <= z by BCIALG_1:3;