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