set A = IntRel L;
let x, y, z, u be Element of L; :: according to WAYBEL_4:def 5 :: thesis: ( u <= x & [x,y] in IntRel L & y <= z implies [u,z] in IntRel L )
assume that
A1: u <= x and
A2: [x,y] in IntRel L and
A3: y <= z ; :: thesis: [u,z] in IntRel L
x <= y by A2, ORDERS_2:def 9;
then u <= y by A1, ORDERS_2:26;
then u <= z by A3, ORDERS_2:26;
hence [u,z] in IntRel L by ORDERS_2:def 9; :: thesis: verum