let L be Lattice; :: thesis: ( L is finite implies L is upper-bounded )
assume L is finite ; :: thesis: L is upper-bounded
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:18;
then A2: a [= c by Th44;
hence c "\/" a = c by LATTICES:def 3; :: thesis: a "\/" c = c
thus a "\/" c = c by A2, LATTICES:def 3; :: thesis: verum