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

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

end;

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

now

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
A5: x in the carrier of (CompactSublatt L) and
A6: 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 L' = CompactSublatt L as non empty full SubRelStr of L by A5;
reconsider x' = x, y' = y as Element of L' by A5, A6;
A7: ex_inf_of {x',y'},L' by A4, YELLOW_0:21;
set X = compactbelow (inf {x,y});
( not compactbelow (inf {x,y}) is empty & compactbelow (inf {x,y}) is directed ) by Def4;
then A8: ex_sup_of compactbelow (inf {x,y}),L by WAYBEL_0:75;

now

let d be set ; :: thesis: ( d in compactbelow (inf {x,y}) implies d in the carrier of L' )
assume d in compactbelow (inf {x,y}) ; :: thesis: d in the carrier of L'
then consider d' being Element of L such that
A9: ( d' = d & inf {x,y} >= d' & d' is compact ) ;
thus d in the carrier of L' by A9, Def1; :: thesis: verum

end;

then A10: compactbelow (inf {x,y}) c= the carrier of L' by TARSKI:def 3;
A11: inf {x,y} = sup (compactbelow (inf {x,y})) by Def3;
reconsider c = "/\" {x,y},L' as Element of L by YELLOW_0:59;

now

let z be set ; :: 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
A12: ( z = z1 & inf {x,y} >= z1 & z1 is compact ) ;
A13: ( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
z1 <= x "/\" y by A12, YELLOW_0:40;
then ( z1 <= x & z1 <= y ) by A13, ORDERS_2:26;
then ( z in compactbelow x & z in compactbelow y ) by A12;
hence z in (compactbelow x) /\ (compactbelow y) by XBOOLE_0:def 4; :: thesis: verum

end;

then A14: compactbelow (inf {x,y}) c= (compactbelow x) /\ (compactbelow y) by TARSKI:def 3;

now

let b' be Element of L'; :: thesis: ( b' in compactbelow (inf {x,y}) implies b' <= "/\" {x,y},L' )
reconsider b = b' as Element of L by YELLOW_0:59;
assume b' in compactbelow (inf {x,y}) ; :: thesis: b' <= "/\" {x,y},L'
then ( b' in compactbelow x & b' in compactbelow y ) by A14, XBOOLE_0:def 4;
then ( b <= x & b <= y ) by Th4;
then ( b' <= x' & b' <= y' ) by YELLOW_0:61;
then b' <= x' "/\" y' by A7, YELLOW_0:19;
hence b' <= "/\" {x,y},L' by A4, YELLOW_0:40; :: thesis: verum

end;

then compactbelow (inf {x,y}) is_<=_than "/\" {x,y},L' by LATTICE3:def 9;
then compactbelow (inf {x,y}) is_<=_than c by A10, YELLOW_0:63;
then A15: sup (compactbelow (inf {x,y})) <= c by A8, YELLOW_0:30;
A16: ( x' in {x,y} & y' in {x,y} ) by TARSKI:def 2;
"/\" {x,y},L' is_<=_than {x,y} by A7, YELLOW_0:31;
then ( "/\" {x,y},L' <= x' & "/\" {x,y},L' <= y' ) by A16, LATTICE3:def 8;
then ( c <= x & c <= y ) by YELLOW_0:60;
then c <= x "/\" y by YELLOW_0:23;
then c <= sup (compactbelow (inf {x,y})) by A11, YELLOW_0:40;
then c = sup (compactbelow (inf {x,y})) by A15, ORDERS_2:25;
hence inf {x,y} in the carrier of (CompactSublatt L) by A11; :: thesis: verum

end;

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