set L = the finite Lattice;
take the finite Lattice ; :: thesis: ( the finite Lattice is noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete )
thus ( the finite Lattice is noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete ) ; :: thesis: verum