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