2. all conditions from Definition 3 are satisfied 3. the graph G2 *is the intersection of all the graphs in the set* {Gb(Ro) : o ∈ O}
4. the graph G3 *is the intersection of all the graphs in the set* {C(G(Ro)) : o ∈ O}
5. observed beforeM = {(x,y,o) : (x,y) *is an edge of the graph* G(Ro)}
6. observed simultM = {(x,y,o) : (x,y) *is an edge of the graph* SA∈Ro K(A)}

Theorem 7 (Satisfiability Theorem for Tgso). If the class Mgso is defined as in Definition 5, then for any model M ∈ Mgso, we have M |= Tgso.

Proof. The fact that M satisfies axioms (2.1) and (2.5) follows from the Theorem 3.

The fact that M satisfies axioms (2.6) and (2.14) follows from the Theorem 5.

Since each Ro is a ranking structure on EO, from the way observed beforeM and observed simultM are defined, we know that M satisfies axioms (2.15) and (2.16).

Since observed simultM is defined from the graphs SA∈Ro K(A) and each graph SA∈Ro K(A) is the incomparability graph of G(Ro), it follows that M |= (2.19). Also since we construct the observed beforeM relation from the graphs G(Ro) and each G(Ro) is a stratified order. Hence, M satisfies axioms (2.17), (2.18) and (2.20) since these axioms are the conditions saying that ✁o is a stratified order for every o and we have G(Ro) = ✁o.

Recall axioms (2.21)-(2.24) together say that

$$(\forall o_{1},o_{2})\left(\begin{array}{c}\text{nonsilutaneous}(o_{1},o_{2})\\ \equiv(\forall o)(\text{observed\_before}(o_{1},o_{2},o)\vee\text{observed\_before}(o_{2},o_{1},o))\end{array}\right)\tag{3.1}$$ $$(\forall o_{1},o_{2})\left(\begin{array}{c}\text{not\_Later\_than}(o_{1},o_{2})\\ \text{observed\_before}(o_{1},o_{2},o)\\ \vee\text{observed\_simult}(o_{1},o_{2},o)\end{array}\right)\tag{3.2}$$
$${\mathrm{~Definition~}}5.$$

But this is equivalent to conditions (2) and (3) from Definition 5. ⊓⊔
Theorem 8 (Axiomatizability Theorem for Tgso). Any model of Tgso is isomorphic to a structure of Mgso.

Proof. Let M be a model of Tgso. We will show that M satisfies the conditions of the structures in Mgso from Definition 3.

Since M satisfies axioms (2.1)–(2.5), from Theorem 4 we can determine the sets E = eventM and the set EO = event occurrenceM , which satisfied the condition (1) of Definition 5.

Since M satisfies axioms (2.6)–(2.14), from Theorem 6 we can determine the graphs G1, G2 and G3 such that the condition (2) of Definition 5 is satisfied.

Let O = event occurrenceM . Then since M satisfies axioms (2.15)–(2.20), we know that for all o the induced relation ✁o is a stratified order, so we can uniquely construct the family of ranking structure F = {Ro : o ∈ O} from the set {✁o : o ∈ O}.

It is easy to check that the condition (5) and (6) of Definition 5 are satisfied.

But since we already know that axioms (2.21)-(2.24) together are equivalent to conditions (3.1) and (3.2) from the proof of Theorem 7, it follows that M satisfies conditions (2) and (3) of Definition 5. ⊓⊔