let L be non empty doubleLoopStr ; :: thesis: ( L is PID implies L is Noetherian )
assume A1: L is PID ; :: thesis: L is Noetherian
let I be Ideal of L; :: according to IDEAL_1:def 26 :: thesis: I is finitely_generated
I is principal by A1;
then consider e being Element of L such that
A2: I = {e} -Ideal ;
take {e} ; :: according to IDEAL_1:def 25 :: thesis: I = {e} -Ideal
thus I = {e} -Ideal by A2; :: thesis: verum