z <x y is in Γ we have by 
laim 5-1 Box+
Γ,x,y ⊆ Box+
Γ,x,z (*). Thus we have:
Box+
Γ,x,z **= Box**+
Γ,x,y . By denition of Γ1 , we also have that y : x¬A is in Γ . By the in lusion (*), we have that z : x¬A must also be in Γ . But z : ¬x¬A ∈ Γ :

ontradi tion, Γ is open. The 
ase where y <x z is in Γ but z <x y is not is symmetri
. (3) Neither y <x z nor z <x y are in Γ . Both formulas has been added by onstru tion of Γ1 . Thus there are some y : ¬x¬A and z : ¬x¬B
in Γ blo
ked by 
ondition 3
. By 
onstru
tion of Γ1 , if y <x z and z <x y were added, then we must have y : x¬B and z : x¬A in Γ . Using 
laim 5-2, if y <x z and z <x y are in Γ1 , then we must have Box+
Γ,x,z ⊆ Box+
Γ,x,y and Box+
Γ,x,y ⊆ Box+
Γ,x,z . Thus Box+
Γ,x,z **= Box**+
Γ,x,y . Thus we have z : x¬B and y : x¬A also in Γ : 
ontradi
tion, Γ is open.

Proof (Claim 3-(I)). We have to he k saturation wrt. (Mod) and (Tx). With regards to (Mod), let u <x z ∈ Γ2 . We have several 
ases: (1) y <x z ∈ Γ :
trivial, Γ being saturated wrt. (Mod).

(2) y <x z ∈ Γ1 but not in Γ , y <x z must have been added by 
onstru
tion of Γ1 . Let u ∈ LabΓ , we have two 
ases: (2a) either u <x z or y <x u are in Γ1 : the saturation 
ondition is then satised. (2b) neither u <x z nor y <x u are in Γ1 . By 
onstru
tion of Γ1 , we have that there is z : ¬x¬A ∈ Γ whi
h is blo ked by v : ¬x¬A by 
ondition 2b, and we have that y : x¬A and y <x v are in Γ . We also have Box+
Γ,x,z ⊆ Box+
Γ,x,y (
laim 5-2). Sin
e x¬A ∈ Box+
Γ,x,y but not in Box+
Γ,x,z (Γ1 would be 
losed), we have that Box+
Γ,x,z ⊂ Box+
Γ,x,y .

As y <x v is in Γ , (Mod) has been applied to it with u so either y <x u or u <x v are in Γ . The rst 
ase 
annot o

ur by our hypothesis, so we have that u <x v is in Γ . (Mod) had also been applied to it with z , so either u <x z is in Γ , or z <x v is in Γ . The rst 
ase being not possible by hypothesis, we have z <x v ∈ Γ , and so Box+
Γ,x,v ⊆ Box+
Γ,x,z (by 
laim 5-1). As v blo
ks z by ondition 3
, we also have Box+
Γ,x,z ⊆ Box+
Γ,x,v (by denition of blo
king ondition). So Box+
Γ,x,v **= Box**+
Γ,x,z , and by denition of Γ2 , as u <x v ∈ Γ ,
u <x z is in Γ2 .

(3) y <x z ∈ Γ2 but not in Γ1 . So y <x z has been added by 
onstru
tion of Γ2 . We then have that there is some y <x v in Γ su
h that Box+
Γ,x,v **= Box**+
Γ,x,z .

Then for all u ∈ LabΓ , we have two 
ases: (3a) Either u <x z or y <x u are in Γ1 : this 
ase is easy. (3b) Neither u <x z nor y <x u are in Γ1 . As y <x v ∈ Γ ,
(Mod) had been applied to it with u: so either y <x u or u <x v are in Γ . The rst ase is impossible by hypothesis, so u <x v is in Γ . As Box+
Γ,x,v **= Box**+
Γ,x,z and by onstru tion of Γ2 , u <x z is then in Γ2 .

As step 2 add some preferential relations y <x z , we have to 
he
k the saturation wrt. (Tx). By denition of Step 2, if y <x z was added in Γ2 , we have Box+
Γ,x,z ⊆ Box+
Γ,x,y , and thus the saturation 
ondition easily follows.

```
Proof (Claim 3-(II)). The 
                          ase of the 
                                     losures 
                                             onditions (i) and (iii) are trivial
                                                                           

```

(as Γ1 is open, and as step 2 only adds preferential formulas). We now 
onsider

```
the 
    ase of the 
               losure 
                      ondition (ii).
                                  

```

Suppose that y <x z and z <x y are in Γ2 . Then we have several 
ases: (1) both formulas are in Γ1 : 
ontradi
tion with the fa
t that Γ1 is open.