INT.Ring is PID by Th97;
hence INT.Ring is Noetherian by Th98; :: thesis: verum