set L = the finite Lattice;
take the finite Lattice ; :: thesis: ( the finite Lattice is co-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 by Lm6;
hence ( the finite Lattice is co-noetherian & the finite Lattice is upper-bounded & the finite Lattice is lower-bounded & the finite Lattice is complete ) ; :: thesis: verum