Theorem lemma7 (D : orientedDigraph) (delta : nat) :
  0 < #|D| -> (forall v : D, delta <= outdeg v) ->
  2 * delta <= ell D \/
  exists S : {set D},
    [/\ S != set0, #|S| <= delta
      & forall v, v \in S -> 2 * delta - ell D <= outdeg_in S v].

Source: theories/applications/ck3/lemma7.v:646

Decoded. In a strong (2.23) oriented digraph that is \(\delta \)-out-regular-from-below (\(d^+(v) \ge \delta \) everywhere, \(\delta \ge 1\)) and where the longest path is short (\(\ell (D) \le 2\delta \)), the vertex set of any longest path supports the structural “kernel” conclusion quantified in the statement — the engine behind the path theorems. (This page quotes the statement in full; the surrounding section fixes the oriented digraph D, \(\delta \), and the strongness/degree hypotheses visible in the quoted text.)