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

proof

let x be Subset of L; :: thesis: ex_sup_of x,L

per cases ( x = {} or x <> {} ) ;

suppose x = {} ; :: thesis: ex_sup_of x,L

hence ex_sup_of x,L by A1, YELLOW_0:42; :: thesis: verum

end;

suppose A2: x <> {} ; :: thesis: ex_sup_of x,L

x is finite by A1, FINSET_1:1;
hence ex_sup_of x,L by A2, YELLOW_0:54; :: thesis: verum

end;

end;

end;

hence L is complete by YELLOW_0:53; :: thesis: verum