set A = IntRel L;
let x, y, z be Element of L; :: according to WAYBEL_4:def 5 :: thesis: ( [x,z] in IntRel L & [y,z] in IntRel L implies [(x "\/" y),z] in IntRel L )
assume that
A1: [x,z] in IntRel L and
A2: [y,z] in IntRel L ; :: thesis: [(x "\/" y),z] in IntRel L
A3: x <= z by A1, ORDERS_2:def 5;
A4: y <= z by A2, ORDERS_2:def 5;
ex q being Element of L st
( x <= q & y <= q & ( for c being Element of L st x <= c & y <= c holds
q <= c ) ) by LATTICE3:def 10;
then x "\/" y <= z by A3, A4, LATTICE3:def 13;
hence [(x "\/" y),z] in IntRel L by ORDERS_2:def 5; :: thesis: verum