let L be algebraic LATTICE; :: thesis: ( L is arithmetic iff CompactSublatt L is LATTICE )
thus ( L is arithmetic implies CompactSublatt L is LATTICE ) :: thesis: ( CompactSublatt L is LATTICE implies L is arithmetic )

proof

set x = the Element of L;
assume A1: L is arithmetic ; :: thesis: CompactSublatt L is LATTICE
not compactbelow the Element of L is empty by Def4;
then consider z being object such that
A2: z in compactbelow the Element of L by XBOOLE_0:def 1;
ex z9 being Element of L st
( z9 = z & the Element of L >= z9 & z9 is compact ) by A2;
then CompactSublatt L is non empty full meet-inheriting join-inheriting SubRelStr of L by A1, Def1;
hence CompactSublatt L is LATTICE ; :: thesis: verum

end;

assume A3: CompactSublatt L is LATTICE ; :: thesis: L is arithmetic

now :: thesis: 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; :: thesis: ( 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
A4: x in the carrier of (CompactSublatt L) and
A5: y in the carrier of (CompactSublatt L) and
ex_inf_of {x,y},L ; :: thesis: inf {x,y} in the carrier of (CompactSublatt L)
reconsider L9 = CompactSublatt L as non empty full SubRelStr of L by A4;
reconsider x9 = x, y9 = y as Element of L9 by A4, A5;
set X = compactbelow (inf {x,y});
reconsider c = "/\" ({x,y},L9) as Element of L by YELLOW_0:58;
A6: inf {x,y} = sup (compactbelow (inf {x,y})) by Def3;
( not compactbelow (inf {x,y}) is empty & compactbelow (inf {x,y}) is directed ) by Def4;
then A7: ex_sup_of compactbelow (inf {x,y}),L by WAYBEL_0:75;
A8: ex_inf_of {x9,y9},L9 by A3, YELLOW_0:21;
then A9: "/\" ({x,y},L9) is_<=_than {x,y} by YELLOW_0:31;

now :: thesis: for z being object st z in compactbelow (inf {x,y}) holds
z in (compactbelow x) /\ (compactbelow y)

let z be object ; :: thesis: ( z in compactbelow (inf {x,y}) implies z in (compactbelow x) /\ (compactbelow y) )
assume z in compactbelow (inf {x,y}) ; :: thesis: z in (compactbelow x) /\ (compactbelow y)
then consider z1 being Element of L such that
A10: z = z1 and
A11: inf {x,y} >= z1 and
A12: z1 is compact ;
A13: z1 <= x "/\" y by A11, YELLOW_0:40;
x "/\" y <= y by YELLOW_0:23;
then z1 <= y by A13, ORDERS_2:3;
then A14: z in compactbelow y by A10, A12;
x "/\" y <= x by YELLOW_0:23;
then z1 <= x by A13, ORDERS_2:3;
then z in compactbelow x by A10, A12;
hence z in (compactbelow x) /\ (compactbelow y) by A14, XBOOLE_0:def 4; :: thesis: verum

end;

then A15: compactbelow (inf {x,y}) c= (compactbelow x) /\ (compactbelow y) ;

now :: thesis: for b9 being Element of L9 st b9 in compactbelow (inf {x,y}) holds
b9 <= "/\" ({x,y},L9)

let b9 be Element of L9; :: thesis: ( b9 in compactbelow (inf {x,y}) implies b9 <= "/\" ({x,y},L9) )
reconsider b = b9 as Element of L by YELLOW_0:58;
assume A16: b9 in compactbelow (inf {x,y}) ; :: thesis: b9 <= "/\" ({x,y},L9)
then b9 in compactbelow y by A15, XBOOLE_0:def 4;
then b <= y by Th4;
then A17: b9 <= y9 by YELLOW_0:60;
b9 in compactbelow x by A15, A16, XBOOLE_0:def 4;
then b <= x by Th4;
then b9 <= x9 by YELLOW_0:60;
then b9 <= x9 "/\" y9 by A8, A17, YELLOW_0:19;
hence b9 <= "/\" ({x,y},L9) by A3, YELLOW_0:40; :: thesis: verum

end;

then A18: compactbelow (inf {x,y}) is_<=_than "/\" ({x,y},L9) by LATTICE3:def 9;

now :: thesis: for d being object st d in compactbelow (inf {x,y}) holds
d in the carrier of L9

let d be object ; :: thesis: ( d in compactbelow (inf {x,y}) implies d in the carrier of L9 )
assume d in compactbelow (inf {x,y}) ; :: thesis: d in the carrier of L9
then ex d9 being Element of L st
( d9 = d & inf {x,y} >= d9 & d9 is compact ) ;
hence d in the carrier of L9 by Def1; :: thesis: verum

end;

then compactbelow (inf {x,y}) c= the carrier of L9 ;
then compactbelow (inf {x,y}) is_<=_than c by A18, YELLOW_0:62;
then A19: sup (compactbelow (inf {x,y})) <= c by A7, YELLOW_0:30;
y9 in {x,y} by TARSKI:def 2;
then "/\" ({x,y},L9) <= y9 by A9, LATTICE3:def 8;
then A20: c <= y by YELLOW_0:59;
x9 in {x,y} by TARSKI:def 2;
then "/\" ({x,y},L9) <= x9 by A9, LATTICE3:def 8;
then c <= x by YELLOW_0:59;
then c <= x "/\" y by A20, YELLOW_0:23;
then c <= sup (compactbelow (inf {x,y})) by A6, YELLOW_0:40;
then c = sup (compactbelow (inf {x,y})) by A19, ORDERS_2:2;
hence inf {x,y} in the carrier of (CompactSublatt L) by A6; :: thesis: verum

end;

then CompactSublatt L is meet-inheriting by YELLOW_0:def 16;
hence L is arithmetic ; :: thesis: verum