:: deftheorem Def26 defines Noetherian IDEAL_1:def 26 :
for L being non empty doubleLoopStr holds
( L is Noetherian iff for I being Ideal of L holds I is finitely_generated );