:: deftheorem Def4 defines co-noetherian LATTICE6:def 4 :
for L being Lattice holds
( L is co-noetherian iff (LattPOSet L) ~ is well_founded );