set A = IntRel L;
let x, y, z, u be Element of L; :: according to WAYBEL_4:def 4 :: 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 5;
then u <= y by A1, ORDERS_2:3;
then u <= z by A3, ORDERS_2:3;
hence [u,z] in IntRel L by ORDERS_2:def 5; :: thesis: verum