let L1 be finite LATTICE; :: thesis: L1 is arithmetic
thus for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def 4,WAYBEL_8:def 5 :: thesis: ( L1 is up-complete & L1 is satisfying_axiom_K & CompactSublatt L1 is meet-inheriting )
thus L1 is up-complete ; :: thesis: ( L1 is satisfying_axiom_K & CompactSublatt L1 is meet-inheriting )
thus L1 is satisfying_axiom_K :: thesis: CompactSublatt L1 is meet-inheriting

proof

let x be Element of L1; :: according to WAYBEL_8:def 3 :: thesis: x = "\/" (compactbelow x),L1
for y being Element of L1 st y in compactbelow x holds
y <= x by WAYBEL_8:4;
then A1: x is_>=_than compactbelow x by LATTICE3:def 9;

now

let y be Element of L1; :: thesis: ( y is_>=_than compactbelow x implies x <= y )
assume A2: y is_>=_than compactbelow x ; :: thesis: x <= y
x in compactbelow x by Th14;
hence x <= y by A2, LATTICE3:def 9; :: thesis: verum

end;

hence x = "\/" (compactbelow x),L1 by A1, YELLOW_0:30; :: thesis: verum

end;

thus CompactSublatt L1 is meet-inheriting :: thesis: verum

proof

let x, y be Element of L1; :: according to YELLOW_0:def 16 :: thesis: ( not x in the carrier of (CompactSublatt L1) or not y in the carrier of (CompactSublatt L1) or not ex_inf_of {x,y},L1 or "/\" {x,y},L1 in the carrier of (CompactSublatt L1) )
assume that
x in the carrier of (CompactSublatt L1) and
y in the carrier of (CompactSublatt L1) and
ex_inf_of {x,y},L1 ; :: thesis: "/\" {x,y},L1 in the carrier of (CompactSublatt L1)
x "/\" y is compact by WAYBEL_3:17;
then x "/\" y in the carrier of (CompactSublatt L1) by WAYBEL_8:def 1;
hence "/\" {x,y},L1 in the carrier of (CompactSublatt L1) by YELLOW_0:40; :: thesis: verum

end;