let L be Lattice; :: thesis: ( L is noetherian iff L .: is co-noetherian )
set R = LattPOSet L;
set Ri = (LattPOSet L) ~ ;
A1: now :: thesis: ( L .: is co-noetherian implies L is noetherian )
A2: (LattPOSet L) ~ = LattPOSet (L .:) by LATTICE3:20;
assume L .: is co-noetherian ; :: thesis: L is noetherian
then ((LattPOSet L) ~) ~ is well_founded by A2;
then LattPOSet L is well_founded by LATTICE3:8;
hence L is noetherian ; :: thesis: verum
end;
now :: thesis: ( L is noetherian implies L .: is co-noetherian )
assume L is noetherian ; :: thesis: L .: is co-noetherian
then LattPOSet L is well_founded ;
then A3: ((LattPOSet L) ~) ~ is well_founded by LATTICE3:8;
(LattPOSet L) ~ = LattPOSet (L .:) by LATTICE3:20;
hence L .: is co-noetherian by A3; :: thesis: verum
end;
hence ( L is noetherian iff L .: is co-noetherian ) by A1; :: thesis: verum