Proof: It is easy to see that if M1 ⊆ M2, then for any clause C = p → l1X1, . . . , lmXm, X1u1**, . . . X**mlm, M2 |= Xiuiimplies M1 |= Xiui. Thus it follows that PM2 ⊆ PM1 and hence

```
lfp(TPM2
          
          ) ⊆ lfp(TPM1
                         
                         ). ✷

```

Proposition 5.4 Let P be a normal propositional CC -program and M be a set of atoms. Then CCGLP (M) = {p : there exists a P-proof scheme S such that M *admits* S,
and p *is the conclusion of* S}
Proof: Let us assume that p ∈ **CCGL**P (M), i.e. p ∈ lfp(TPM ). Since lfp(TPM ) =
Sn≥1 T
n PM
(∅), we can easily show by induction on n that if p ∈ T
n PM
(∅), then there is a P-CC -proof scheme Sp such p is the conclusion of Sp and Sp is admitted by M.

Conversely, we can show, by induction on the length of the P-CC -proof schemes, that whenever there is P-CC -proof scheme S admitted by M, then p belongs to lfp(TPM ). ✷
Next we prove that analogue of Proposition 4.4.

Proposition 5.5 For every normal CC -program P*, the operator* **CCGL**P *is lowerhalf continuous.*
Proof: We need to prove that for every normal CC -program P and every monotonically decreasing sequence hXnin∈N

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

We need to prove two inclusions: ⊆, and ⊇.

We first show ⊇. Since
\
j∈N
Xj ⊆ Xn for every n ∈ N, it follows from the antimonotonicity of **CCGL**P that we have

$$\mathbb{L}_{X}$$

CCGLP (Xn) ⊆ GLP (\
j∈N
Xj ).

As n is arbitrary,

$$\bigcup_{n\in N}C C G L_{P}(X_{n})\subseteq C C G L_{P}(\bigcap_{j\in N}X_{j}).$$
$$17$$
