let L be LATTICE; :: thesis: ( L is trivial implies L is arithmetic )
assume A1: L is trivial ; :: thesis: L is arithmetic
reconsider L9 = L as 1 -element LATTICE by A1;
A2: for x, y being Element of L9 st x << y holds
ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
proof
let x, y be Element of L9; :: thesis: ( x << y implies ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y ) )
assume A3: x << y ; :: thesis: ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
take k = x; :: thesis: ( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
x = y by STRUCT_0:def 10;
then k is compact by A3, WAYBEL_3:def 2;
hence k in the carrier of (CompactSublatt L9) by Def1; :: thesis: ( x <= k & k <= y )
thus ( x <= k & k <= y ) by STRUCT_0:def 10; :: thesis: verum
end;
A4: L9 is algebraic by Th7, A2;
for z, v being Element of L9 st z in the carrier of (CompactSublatt L9) & v in the carrier of (CompactSublatt L9) & ex_inf_of {z,v},L9 holds
inf {z,v} in the carrier of (CompactSublatt L9) by STRUCT_0:def 10;
then CompactSublatt L9 is meet-inheriting by YELLOW_0:def 16;
hence L is arithmetic by A4; :: thesis: verum