Two Seymour vertices in every sink-free oriented graph

We prove, relative to two explicitly stated results of the pinned OpenAI manuscript on Seymour's conjecture, that every nonempty finite sink-free oriented graph has two distinct vertices whose exact second out-neighborhood is at least as large as their first. This is Conjecture 2 of Dara, Francis, Jacob and Narayanan. The inputs are the ordinary one-vertex Seymour theorem and a finite-relation pruning lemma; their truth is stipulated here. A minimum counterexample has a unique good vertex with one successor. Deleting that vertex leaves weak subset deficits together with a strict inequality for subsets that do not reach the successor in one or two steps. In a transitive blowup, compatibility with the diagonal selects many fibers with this strict inequality. Their total gain dominates the possible losses of all remaining fibers, allowing the established pruning objective to close. All deductions from the two inputs are proved below. Finite diagnostics and formal supporting lemmas are distinguished from the full graph theorem.