let L be LATTICE; :: thesis: ( L is trivial implies L is arithmetic )
assume L is trivial ; :: thesis: L is arithmetic
then reconsider L' = L as trivial LATTICE ;
for x, y being Element of L' st x << y holds
ex k being Element of L' st
( k in the carrier of (CompactSublatt L') & x <= k & k <= y )

proof

let x, y be Element of L'; :: thesis: ( x << y implies ex k being Element of L' st
( k in the carrier of (CompactSublatt L') & x <= k & k <= y ) )
A1: x = y by STRUCT_0:def 10;
assume A2: x << y ; :: thesis: ex k being Element of L' st
( k in the carrier of (CompactSublatt L') & x <= k & k <= y )
take k = x; :: thesis: ( k in the carrier of (CompactSublatt L') & x <= k & k <= y )
k is compact by A1, A2, WAYBEL_3:def 2;
hence k in the carrier of (CompactSublatt L') by Def1; :: thesis: ( x <= k & k <= y )
thus ( x <= k & k <= y ) by STRUCT_0:def 10; :: thesis: verum

end;

then A3: L' is algebraic by Th7;
for z, v being Element of L' st z in the carrier of (CompactSublatt L') & v in the carrier of (CompactSublatt L') & ex_inf_of {z,v},L' holds
inf {z,v} in the carrier of (CompactSublatt L') by STRUCT_0:def 10;
then CompactSublatt L' is meet-inheriting by YELLOW_0:def 16;
hence L is arithmetic by A3, Def5; :: thesis: verum