let L be Lattice; :: thesis: ( L is finite implies L is upper-bounded )
assume L is finite ; :: thesis: L is upper-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 = FinJoin B,(id the carrier of L); :: according to LATTICES:def 14 :: 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 )
a [= (id the carrier of L) . a by FUNCT_1:35;
then A1: ( a [= c & c "\/" a = a "\/" c ) by Th44;
hence c "\/" a = c by LATTICES:def 3; :: thesis: a "\/" c = c
thus a "\/" c = c by A1, LATTICES:def 3; :: thesis: verum