theorem Th1: :: BCIALG_5:1

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;