:: deftheorem Def1 defines Noetherian ABCMIZ_0:def 1 :
for T being RelStr holds
( T is Noetherian iff the InternalRel of T is co-well_founded );