consider L being finite Lattice;
take L ; :: thesis: ( L is noetherian & L is upper-bounded & L is lower-bounded & L is complete )
LattPOSet L is well_founded ;
hence ( L is noetherian & L is upper-bounded & L is lower-bounded & L is complete ) by Def3; :: thesis: verum