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 )
LattPOSet the finite Lattice is well_founded ;
hence ( the finite Lattice is noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete ) by Def3; :: thesis: verum