set A = IntRel L;
take IntRel L ; :: thesis: IntRel L is auxiliary
thus IntRel L is auxiliary(i) by ORDERS_2:def 5; :: according to WAYBEL_4:def 7 :: thesis: ( IntRel L is auxiliary(ii) & IntRel L is auxiliary(iii) & IntRel L is auxiliary(iv) )
thus IntRel L is auxiliary(ii) :: thesis: ( IntRel L is auxiliary(iii) & IntRel L is auxiliary(iv) )

proof

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

end;

thus IntRel L is auxiliary(iii) :: thesis: IntRel L is auxiliary(iv)

proof

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
A4: [x,z] in IntRel L and
A5: [y,z] in IntRel L ; :: thesis: [(x "\/" y),z] in IntRel L
A6: x <= z by A4, ORDERS_2:def 5;
A7: y <= z by A5, 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 A6, A7, LATTICE3:def 13;
hence [(x "\/" y),z] in IntRel L by ORDERS_2:def 5; :: thesis: verum

end;

thus IntRel L is auxiliary(iv) by YELLOW_0:44, ORDERS_2:def 5; :: thesis: verum