:: deftheorem Def3 defines noetherian LATTICE6:def 3 :
for L being Lattice holds
( L is noetherian iff LattPOSet L is well_founded );