let L be Lattice; :: thesis: ( L is noetherian iff L .: is co-noetherian )
set R = LattPOSet L;
set Ri = (LattPOSet L) ~ ;

A1: now

assume L is noetherian ; :: thesis: L .: is co-noetherian
then LattPOSet L is well_founded by Def3;
then A2: ((LattPOSet L) ~ ) ~ is well_founded by LATTICE3:8;
(LattPOSet L) ~ = LattPOSet (L .: ) by LATTICE3:20;
hence L .: is co-noetherian by A2, Def4; :: thesis: verum

end;

now

assume A3: L .: is co-noetherian ; :: thesis: L is noetherian
(LattPOSet L) ~ = LattPOSet (L .: ) by LATTICE3:20;
then ((LattPOSet L) ~ ) ~ is well_founded by A3, Def4;
then LattPOSet L is well_founded by LATTICE3:8;
hence L is noetherian by Def3; :: thesis: verum

end;

hence ( L is noetherian iff L .: is co-noetherian ) by A1; :: thesis: verum