theorem Th12: :: WAYBEL31:12

for L1 being finite LATTICE holds L1 is arithmetic