Proof**. We show the equivalence between (b) and (d). From (b) to (d) is clear,**
and from (d) to (b) follows immediately from Propositiond 4.

For instance, for the program in (10), the loop formula of non-elementary loop
{p, q, r} (the last one in (13)) can be disregarded in view of Theoremd **1 (d).**

## 3.3 Elementarily Unfounded Sets For Disjunctive Programs

Let Π be a disjunctive program. For any sets X, Y of atoms, by ΠX,Y **we denote**
the set of all rules (12) of Π such that X |= B, F and X ∩ (A \ Y ) = ∅**. That is,**
the program ΠX,Y contains all rules of Π that can provide supports for Y **w.r.t.** X.

If Y = X, we also denote ΠX,Y by ΠX **. When Π is a nondisjunctive program,**
this definition reduces to the definition of ΠX **for nondisjunctive programs given**
earlier. Furthermore, when Π is nondisjunctive and Y **is not a singleton, then** Y is an elementary loop of ΠX,Y iff Y **is an elementary loop of Π**X .

We extend the definition of an elementarily unfounded set to disjunctive programs by replacing "ΠX" with "ΠX,Y ": for a disjunctive program Π and a set X **of atoms,**
we say that a set Y of atoms that occur in Π is elementarily unfounded **by Π w.r.t.** X
if Y is
- an elementary loop of ΠX,Y **that is unfounded by Π w.r.t.** X or
- **a singleton that is unfounded by Π w.r.t.** X.

It is clear from the definition that every elementarily unfounded set **for Π w.r.t.** X is an elementary loop of Π and that it is also unfounded by Π w.r.t. X.

For instance, let Π be the program (10). The program Π{p,q,r},{p,q} **consists of**
the first rule in (10), so that {p, q} is not an elementary loop of Π{p,q,r},{p,q}**. On**
the other hand, Π{p,q},{p,q} consists of the last two rules in (10), and {p, q} **is an**
elementary loop of Π{p,q},{p,q}. Since {p, q} is also unfounded by Π w.r.t. {p, q}**, it**
is an elementarily unfounded set for Π w.r.t. {**p, q**}.

Proposition 5, Corollary 1, and Theorem 2 remain correct after replacing "nondisjunctive program" in their statements with "disjunctive program," and "ΠX**" with**
"ΠX,Y ."
Propositiond 5 For any disjunctive program Π, any set X **of atoms, and any elementary loop** Y of ΠX,Y , X satisfies ES Π(Z**) for all nonempty proper subsets** Z of Y . Proof. From the fact that Y is an elementary loop of ΠX,Y **, it follows that any**
nonempty proper subset Z of Y is outbound in Y for ΠX,Y . If Y **is not a singleton,**
this implies that Y is a subset of X **and that, for each nonempty proper subset** Z
of Y **, there is a rule (12) in Π such that**

$A\cap Z\neq\emptyset$ , . 
$\left(32\right)$ . 
A ∩ Z 6= ∅ , **(31)**
$$A\cap(Y\setminus Z)=\varnothing\ ,$$
A ∩ (Y \ Z) = ∅ , **(32)**
$$B\cap Z=\varnothing\ ,$$
$\left(33\right)$ . 
B ∩ Z = ∅ , **(33)**
$$X\models B,F\ ,$$
X |= B, F , (34)