  A directed graph $D=(V(D),A(D))$ has a kernel if there exists an independent
set $K\subseteq V(D)$ such that every vertex $v\in V(D)-K$ has an ingoing arc
$u\mathbin{\longrightarrow}v$ for some $u\in K$. There are directed graphs that
do not have a kernel (e.g. a 3-cycle). A quasi-kernel is an independent set $Q$
such that every vertex can be reached in at most two steps from $Q$. Every
directed graph has a quasi-kernel. A conjecture by P.L. Erd\H{o}s and L.A.
Sz\'ekely (cf. A. Kostochka, R. Luo, and, S. Shan, arxiv:2001.04003v1, 2020)
postulates that every source-free directed graph has a quasi-kernel of size at
most $|V(D)|/2$, where source-free refers to every vertex having in-degree at
least one. In this note it is shown that every source-free directed graph that
has a kernel also has a quasi-kernel of size at most $|V(D)|/2$, by means of an
induction proof. In addition, all definitions and proofs in this note are
formally verified by means of the Coq proof assistant.
