Let Γ be an open and saturated set under blo
king. We will 
onstru
t the set Γ
∗
from Γ in three steps. First, we 
onsider formulas z : ¬x¬A whi
h are

```
blo
  ked by 
         ondition 3
                  (and not by 3b). We 
                                  onstru
                                       t a set Γ1 from Γ whi
h

```

satises the saturation ondition (Fx) wrt. these formulas.

Step 1. For ea h formula z : ¬x¬A ∈ Γ for whi
h 
ondition (Fx) is not

```
fullled and that is blo
                       ked only by 
                                    ondition 3
                                               , we 
                                                    onsider the oldest label
                                                                           
u that blo
ks the formula. Therefore, the formula u : ¬x¬A is in Γ and it is

```

not blo ked by ondition 3 6
. Sin e z : ¬x¬A is not blo
ked by 
ondition 3b, u : ¬x¬A is not blo
ked for this 
ondition either, and thus the rule (F2x)
has been applied to it. Hen e there exists a label y su
h that y : **A, y** : x¬A
and y <x u are in Γ . We then add y <x z to Γ . We 
all Γ1 the resulting set.

Claim 2. (I) Γ1 is saturated, ex
ept for (Mod) and the formulas x : ¬(A ⇔ B)
and z : ¬x¬A respe
tively blo
ked by 
ondition 2b and 3b. (II) It is open.

The step 2 will now build a set Γ2 saturated wrt. (Mod) from Γ1 .

Step 2. For ea h y <x z ∈ Γ , if Box+
Γ,x,z ⊂ Box+
Γ,x,y , then for ea
h z0 su
h that Box+
Γ,x,z0 **= Box**+
Γ,x,z we add y <x z0 to Γ1 . We 
all Γ2 the resulting set.

Claim 3. (I) Γ2 is saturated ex
ept for the formulas x : ¬(A ⇔ B) and z :
¬x¬A respe
tively blo
ked by 
ondition 2b and 3b. (II) It is open.

```
We will now 
         onsider the formulas blo
                         ked by 
                               onditions 2b and 3b, and
                                               

```

nally build a set Γ3 saturated wrt. all rules from Γ2 .

Step 3. For ea h label x su
h that there is a formula x : ¬(A ⇔ B) ∈ Γ or z : ¬x¬A ∈ Γ respe
tively blo
ked by 
ondition 2b or 3b, we let u be the oldest label whi h aused the blo king. We then onstru t the set Γ3 by the following pro edure:

1. we remove from Γ2 ea
h relation <x , and all formulas v : ¬x¬A and v :
x¬A (v ∈ LabΓ ).

2. For all label z ∈ LabΓ su
h that z 6= x, we add x <x z .

3. For all labels z, v ∈ LabΓ su
h that z 6= x, if v <u z ∈ Γ2 , then we add v <x z .

4. For ea h v : u¬A ∈ Γ , if A ∈ ΠΓ (x) we then add v : x¬A.

5. For ea h v : ¬u¬A ∈ Γ su
h that v 6= x, we add v : ¬u¬A
6. For ea h formula A ∈ ΠΓ (x), we add x : xA.
Claim 4. (I) Γ3 is saturated wrt. al l rules. (II) It is open.

```
  We then let Γ
           ∗ = Γ3 . It is easy to see that for all formulas A ∈ LCSL , if
x : A ∈ Γ then x : A ∈ Γ
                  ∗
                   , as none of these formulas are removed by the
                                                  
onstru
     tion of Γ
           ∗
           .
            
  We now prove the pre
                edent 
                     laims.
                        
6

 If it was, let v older than u the label whi
h 
auses the blo
king. Then v will also blo
k
 u : ¬x¬A, 
ontradi
tion, as u is by hypothesis the oldest label blo
king z : ¬x¬A.

```
