let L be finite Lattice; :: thesis: ( L is noetherian & L is co-noetherian )
(LattPOSet L) ~ is well_founded by Lm6;
hence ( L is noetherian & L is co-noetherian ) by Def3, Def4; :: thesis: verum