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