let L be lower-bounded algebraic LATTICE; ( L is arithmetic iff L -waybelow is multiplicative )
thus
( L is arithmetic implies L -waybelow is multiplicative )
( L -waybelow is multiplicative implies L is arithmetic )proof
assume A1:
L is
arithmetic
;
L -waybelow is multiplicative
now for a, x, y being Element of L st [a,x] in L -waybelow & [a,y] in L -waybelow holds
[a,(x "/\" y)] in L -waybelow reconsider C =
CompactSublatt L as non
empty full meet-inheriting SubRelStr of
L by A1;
let a,
x,
y be
Element of
L;
( [a,x] in L -waybelow & [a,y] in L -waybelow implies [a,(x "/\" y)] in L -waybelow )assume that A2:
[a,x] in L -waybelow
and A3:
[a,y] in L -waybelow
;
[a,(x "/\" y)] in L -waybelow
a << x
by A2, WAYBEL_4:def 1;
then consider c being
Element of
L such that A4:
c in the
carrier of
(CompactSublatt L)
and A5:
a <= c
and A6:
c <= x
by Th7;
a << y
by A3, WAYBEL_4:def 1;
then consider k being
Element of
L such that A7:
k in the
carrier of
(CompactSublatt L)
and A8:
a <= k
and A9:
k <= y
by Th7;
A10:
c "/\" k <= x "/\" y
by A6, A9, YELLOW_3:2;
reconsider c9 =
c,
k9 =
k as
Element of
C by A4, A7;
c9 "/\" k9 in the
carrier of
(CompactSublatt L)
;
then
c "/\" k in the
carrier of
(CompactSublatt L)
by YELLOW_0:69;
then
c "/\" k is
compact
by Def1;
then A11:
c "/\" k << c "/\" k
by WAYBEL_3:def 2;
a "/\" a = a
by YELLOW_5:2;
then
a <= c "/\" k
by A5, A8, YELLOW_3:2;
then
a << x "/\" y
by A10, A11, WAYBEL_3:2;
hence
[a,(x "/\" y)] in L -waybelow
by WAYBEL_4:def 1;
verum end;
hence
L -waybelow is
multiplicative
by WAYBEL_7:def 7;
verum
end;
assume A12:
L -waybelow is multiplicative
; L is arithmetic
now for x, y being Element of L st x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L holds
inf {x,y} in the carrier of (CompactSublatt L)let x,
y be
Element of
L;
( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) )assume that A13:
x in the
carrier of
(CompactSublatt L)
and A14:
y in the
carrier of
(CompactSublatt L)
and
ex_inf_of {x,y},
L
;
inf {x,y} in the carrier of (CompactSublatt L)
y is
compact
by A14, Def1;
then
y << y
by WAYBEL_3:def 2;
then A15:
[y,y] in L -waybelow
by WAYBEL_4:def 1;
x is
compact
by A13, Def1;
then
x << x
by WAYBEL_3:def 2;
then
[x,x] in L -waybelow
by WAYBEL_4:def 1;
then
[(x "/\" y),(x "/\" y)] in L -waybelow
by A12, A15, WAYBEL_7:41;
then
x "/\" y << x "/\" y
by WAYBEL_4:def 1;
then
x "/\" y is
compact
by WAYBEL_3:def 2;
then
x "/\" y in the
carrier of
(CompactSublatt L)
by Def1;
hence
inf {x,y} in the
carrier of
(CompactSublatt L)
by YELLOW_0:40;
verum end;
then
CompactSublatt L is meet-inheriting
by YELLOW_0:def 16;
hence
L is arithmetic
; verum