Our goal is to prove two inclusions: ⊆, and ⊇.

We first show ⊇. Since

$$\bigcap_{j\in N}X_{j}\subseteq X_{n}$$
$n\in N$, by antimu
for every n ∈ N, by antimonotonicity of GLP we have

$$\mathbf{r}^{\mathrm{f}}$$
$$G L_{P}(X_{n})\subseteq G L_{P}(\bigcap_{j\in N}X_{j}).$$
$${\mathrm{As~}}n{\mathrm{~is~arbitrary}},$$
arbitrary,  $$\bigcup_{n\in N}GL_{P}(X_{n})\subseteq GL_{P}(\bigcap_{j\in N}X_{j}).$$  a inclusion $\supset$ holds.  
Thus the inclusion ⊇ holds.

Conversely, let p ∈ GLP (Tn∈N Xn). Then, by Proposition 4.3, there must be a proof scheme S with support support U and conclusion p such that

$$U\cap\bigcap_{n\in N}X_{n}=\varnothing.$$

But the family hXnin∈n is monotonically descending and the set U is finite. Thus there is an integer n0 so that U ∩ Xn0 = ∅.

This, however, implies that p ∈ GLP (Xn0

), and thus

$$p\in\bigcup_{n\in N}G L_{P}(X_{n}).$$
$${}_{P}(\bigcap_{n\in N}X_{n})=\bigcup_{n\in N}\,G L_{P}(X_{n})$$

As p is arbitrary, the inclusion ⊆ holds. Thus GLP (Tn∈N Xn) = Sn∈N GLP (Xn).

✷

The lower-half continuity of antimonotone operators is closely related to programs, as shown in the following result.

Proposition 4.5 Let At be a denumerable set of atoms. Let f *be an antimonotone* and lower-half continuous operator on P(At)*. Then there exists a normal logic* program P *such that* f = GLP .

Proof.

We define the program P = Pf as follows:

$$P=\{p\leftarrow\neg q_{1},\ldots,\neg q_{i}:p\in f(At\setminus\{q_{1},\ldots,q_{i}\})\}.$$  We claim that $f=GL_{P}$, that is, for all $X$, $f(X)=GL_{P}(X)$.  
10