set A = IntRel L;
take
IntRel L
; IntRel L is auxiliary
thus
IntRel L is auxiliary(i)
by ORDERS_2:def 5; WAYBEL_4:def 7 ( IntRel L is auxiliary(ii) & IntRel L is auxiliary(iii) & IntRel L is auxiliary(iv) )
thus
IntRel L is auxiliary(ii)
( IntRel L is auxiliary(iii) & IntRel L is auxiliary(iv) )proof
let x,
y,
z,
u be
Element of
L;
WAYBEL_4:def 4 ( 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
;
[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;
verum
end;
thus
IntRel L is auxiliary(iii)
IntRel L is auxiliary(iv) proof
let x,
y,
z be
Element of
L;
WAYBEL_4:def 5 ( [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
;
[(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;
verum
end;
thus
IntRel L is auxiliary(iv)
by YELLOW_0:44, ORDERS_2:def 5; verum