How are theories represented using Conceptual Graphs?

Question

Theory 1 shows three axioms and two definitions, written in First Order Logic (FOL), that represents a fragment of a mereology theory. For this posting, it is important that the set of axioms is considered as a theory (i.e. a set of axioms together with theorems as a logical consequence of those axioms). In the context of this question, the particular axioms are not significant. Any other set of axioms forming a consistent theory would be equally acceptable.

Theory 1

Axioms

Reflexivity $\forall x : part(x,x)$

Antisymmetry $\forall x \forall y : ((part(x,y) \land part(y,x)) \implies (x = y))$

Transitivity $\forall x \forall y \forall z :((part(x,y) \land part(y,z)) \implies part(x,z))$

Definitions

Overlap : $\forall x,y \colon (overlap(x,y) \iff(\exists z \colon (part(z,x) \land part(z,y)))$

Proper Part : $\forall x,y \colon (proprPart(x,y) \iff (part(x,y) \land \neg part(y,x)))$

I am using CafeOBJ to represent the above logical axioms and definitions, shown in Listing 1:

Listing 1

   mod M{
    [E]
    preds overlap part properPart : E E
 -- axioms
 ax [M1] : \A[x:E] part(x,x) .  
 ax [M2] : \A[x:E]\A[y:E] ((part(x,y) & part(y,x)) -> (x = y))  .
 ax [M3] : \A[x:E]\A[y:E]\A[z:E]((part(x,y) & part(y,z))  -> part(x,z)) .
 -- definitions
 ax [DM1] : \A[x:E]\A[y:E] (properPart(x,y) <-> (part(x,y) & ~(part(y,x)))) .  
 ax [DM2] : \A[x:E]\A[y:E] (overlap(x,y) <->  (\E[z:E] (part(z,x) & part(z,y)))) .  
    }

Note that the logical theory is contained in a named module called M. The variables are over a domain of generic entities E, universal and existential quantification are denoted by \A[x:E] and \A[x:E] respectively. In CafeOBJ, named modules allow one to structure signatures, theories, sub/super theories, and models using the Theory of Institutions (TOI).

Below is my naïve attempt to present the axioms as a set of conceptual graphs (CG). My motivation for using CGs is that they provide an intuitive visualization of logic and have a direct relation to Common Logic (ISO zipped PDF).

The above CG was produced using CharGer software as Java zip file (manual).

My understanding of the above CGs is as follows:

1. The variables are universally quantified, not default for CGs, but allowed in extended CG (ECG).
2. The three graphs are all related by conjunction, which is default for GC.
3. The arrow on graph representing reflexivity is bi-directional.
4. Both antisymmetry and transitivity are represented by an IF-THEN contexts.
5. Dotted lines are co-references.
6. Equality (=) is actually commutative, but is represented as a directed relation .
7. Each CG asserts a single proposition, labelled Proposition.

Question:

How do I present Theory 1 using CGs? Do I need some labeling that indicates that a set of concepts represent a theory. Or are theories represented by some enclosing special type of concept?