let L be LATTICE; :: thesis: ( L is finite implies L is complete )

assume A1: L is finite ; :: thesis: L is complete

for x being Subset of L holds ex_sup_of x,L

assume A1: L is finite ; :: thesis: L is complete

for x being Subset of L holds ex_sup_of x,L

proof

hence
L is complete
by YELLOW_0:53; :: thesis: verum
let x be Subset of L; :: thesis: ex_sup_of x,L

end;