INT.Ring is PID by Th94;
hence INT.Ring is Noetherian by Th95; :: thesis: verum