let L be Lattice; :: thesis: ( L is finite implies L is lower-bounded )
assume L is finite ; :: thesis: L is lower-bounded
then reconsider B = the carrier of L as Element of Fin 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 ;
then A1: c [= a by Th41;
hence c "/\" a = c by LATTICES:4; :: thesis: a "/\" c = c
thus a "/\" c = c by A1, LATTICES:4; :: thesis: verum