:: deftheorem Def2 defines Noetherian ABCMIZ_0:def 2 :
for T being non empty RelStr holds
( T is Noetherian iff for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) );