for L1 being finite LATTICE holds L1 is arithmetic