We now apply the hypothesis of the theorem with C = C0 , C
0 = C
0 0
:
Either (a) there exists C1 ∈ D such that p ∈ C1 ⊆ C0 ∨q C
0 0
, or (b) v
∗
p >
minα ∈ C0 ∨q C00
\ {p}
v
∗
α
.

If (b) holds, we arrive to contradiction in the following way:

$$v_{p}^{(n)}\,=\,\min\left(\,\min_{\alpha\in C_{0}\setminus\{q\}}\,v_{\alpha}^{(n-1)}\,,\,\min_{\alpha\in C_{0}^{\prime}}\,v_{\alpha}^{(n-2)}\,\right)\,\leq\,\min_{\alpha\in C_{0}\setminus\{p\}}\,v_{\alpha}^{\star}\,<\,v_{p}^{\star},$$
$$(37)$$
$$(38)$$
, (37)
where we have used the inequalities v
(k) ≤ v
∗.

If (a) holds, we can write

$$\begin{array}{l l}{{v_{p}^{(n)}\,\leq\,\min\left(\,\operatorname*{min}_{\alpha\in C_{1}\cap C_{0}}v_{\alpha}^{(n-1)}\,,\,\operatorname*{min}_{\alpha\in C_{1}\cap C_{0}}v_{\alpha}^{(n-2)}\,,\,\operatorname*{min}_{\alpha\in C_{1}\cap C_{0}^{\prime}}v_{\alpha}^{(n-2)}\,\right)}}\\ {{\qquad\leq\,\operatorname*{min}_{\alpha\in C_{1}}v_{\alpha}^{(n-1)}\,\leq\,v_{p}^{(n)},}}\end{array}$$

where the first inequality derives from (36) because of the inclusion that relates C1 to C0 and C
0 0
, the second inequality uses simply that v
(n−2) ≤
v
(n−1) , and the third one follows from the definition of v
(n)
p since C1 3 p.

Therefore, the three expressions between inequality signs in (38) are in fact equal to each other, which entails that C1 is a realizer. On account of the definition of C˙1 and the equality v
(n)
p = v
∗
p
, the obtained equality entails also that C˙1 ⊆ C1 ∩ C˙0 ⊂ C˙0 , where the last inclusion is strict since q ∈ C˙0 but q /∈ C1 . So, C1 is indeed a realizer with C˙1 strictly contained in C˙0 .

Remarks 1. Condition (b) is satisfied whenever one has v
∗
p > minα ∈ C\ {p} v
∗
α
, which involves neither C
0 nor q .

2. The strategy of the preceding proof is akin to the SL-resolution procedure of logic programming.

For some doctrines whose Blake canonical form does not satisfy v
∗ = v 0 one can still see that suspicious derivations of belief, i. e. from unsatisfiable conjunctions, are never behind the decision of accepting or rejecting certain literals. An interesting example is what can be called the doctrine of existence and uniqueness:

$$(39)$$
$$\bigvee_{p\in I I_{+}}p,$$
$$\mathrm{for~any~two~different~}p,q\in I\!I_{+}.$$
$$(40)$$
p, (39)
$${\overline{{p}}}\,\vee\,{\overline{{q}}},$$
p ∨ q, for any two different *p, q* ∈ Π+. (40)