This question is about synonymy of Morse-Kelley set theory "$\sf MK$" with the following Mereological theory:

Language: first order logic with equality. Extra-logical primitives: $\subseteq$ standing for the binary relation "*is a part of*", and a partial unary function symbol $\{\}$ standing for "*is the label of*", or can also be read as "*is the singleton of*".

Extra-logical Axioms:

**Parthood:** $x \subseteq x \\ x \subseteq y \subseteq x \to x=y \\ x \subseteq y \subseteq z \to x \subseteq z$

**Supplmentation:** $\neg x \subseteq y \to \exists z \subseteq y: \neg z \ O \ x$

*Define:* $atom(x) \iff \forall y \subseteq x \, (y=x)$

**Atomicity:** $\forall x \exists \ atom \ y: y \subseteq x  $

**Composition:** $\exists \ atom \ y: \phi, \to \exists x \forall \ atom \ y \,( y \subseteq x \leftrightarrow \phi); \text{ if } x \text { is not free in } \phi$

*Define:* $(x= \mathcal S \, y: \phi) \iff \forall \ atom \ y \, (y \subseteq x \leftrightarrow \phi)$ 


**Labeling:** $\{x\}=\{y\} \to x=y$

**Purity:** $ \exists x \, (y=\{x\}) \leftrightarrow atom(y)$

**Start:** $\exists a \exists b: a \neq b \land \forall x \,( x=\{x\} \leftrightarrow x=a \lor x = b)$  

**Foundation:** $ \forall x (\{x\} \subseteq h \to x \subseteq h \land \exists y: x=\{y\}) \to \exists a \subseteq h: a=\{a\}$



**Replacement:** $\phi(a,b) \land \phi (a,c) \to b=c \\ \phi(a,b) \to atom(a) \land \exists l: l=\{b\} \\ A = \mathcal S \, a: \exists b \, (\phi(a,b)) \\ B= \mathcal S \, b: \exists a \exists c ( \phi(a,c) \land b \subseteq c ) \\ \to \\ \exists l: l=\{A\} \leftrightarrow \exists l: l= \{B\} $

*Define:* ${\sf Q}= \mathcal S \, a: a=\{a\}$


**Abundance:** $\exists l: l= \{{\sf Q}\}$ 


**Infinity:** $\exists x: x \not \subseteq {\sf Q} \land \forall y: \{y\} \subseteq x \to \{\{y\}\} \subseteq x$

**Choice:** $\exists C \forall x \exists y : y=C(x) \land   \{y\} \subseteq x$

This theory does respect all tenets of Mereology, the first four principles are the axioms of Atomic General Extensional Mereology "$\sf AGEM$". Define set membership $\in$ as:

$$x \in y \iff \exists z \subseteq y: z=\{x\}  $$

Call the collection of all sentences written in $\sf FOL(=,\in)$ over the whole domain of this theory (i.e. all quantifiers unrestricted) that are provable in this theory as "$\sf MMK$", standing for "Mereological $\sf MK$". 

It should be made clear that $\sf MMK$ proves the non-existence of an empty set, minimally breaches Foundation, and that it is fully extensional.

> Is $\sf MMK$ synonymous with $\sf MK$?

> Is $\sf MK$ synonymous with this theory?


Note: "$ O $" stands for the overlap relation (i.e. existence of a common part), and "$\mathcal S \, a: \phi$" stands for "*the sum of all atoms realizing $\phi$*".