set_has_maximal_iff_noetherian source