let L be Lattice; :: thesis: ( L is finite implies L is lower-bounded )
assume L is finite ; :: thesis: L is lower-bounded
then the carrier of L is finite ;
then reconsider B = the carrier of L as Finite_Subset of the carrier of L by FINSUB_1:def 5;
take c = FinMeet B,(id the carrier of L); :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of L holds
( c "/\" b₁ = c & b₁ "/\" c = c )
let a be Element of L; :: thesis: ( c "/\" a = c & a "/\" c = c )
(id the carrier of L) . a [= a by FUNCT_1:35;
then A1: c [= a by Th56;
hence c "/\" a = c by LATTICES:21; :: thesis: a "/\" c = c
thus a "/\" c = c by A1, LATTICES:21; :: thesis: verum