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

set x = the Element of L;
assume A1: L is arithmetic ; :: thesis:
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:

end;

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

let x, y be Element of L; :: thesis:
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:
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;

let z be object ; :: thesis:
assume z in compactbelow (inf {x,y}) ; :: thesis:
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:

end;

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

let b9 be Element of L9; :: thesis:
reconsider b = b9 as Element of L by YELLOW_0:58;
assume A16: b9 in compactbelow (inf {x,y}) ; :: thesis:
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:

end;

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

let d be object ; :: thesis:
assume d in compactbelow (inf {x,y}) ; :: thesis:
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:

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:

end;

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