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)

A1: now :: thesis: for y being Element of L1 st y is_>=_than compactbelow x holds
x <= y

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 Th11;
hence x <= y by A2, LATTICE3:def 9; :: thesis: verum

end;

for y being Element of L1 st y in compactbelow x holds
y <= x by WAYBEL_8:4;
then x is_>=_than compactbelow x by LATTICE3:def 9;
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;