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:** $y\not \subseteq x \to \exists z \subseteq y: \neg z \ O \ x$

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

**Atomicity:** $\forall x \, \exists \text{ atom } y: y \subseteq x  $

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

*Define:* $(x= \mathcal S \, y: \varphi) \iff \forall \text{ atom } y \, (y \subseteq x \leftrightarrow \varphi)$ 


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

**Purity:** $ \exists x \, (y=\{x\}) \leftrightarrow \operatorname{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 \ O  \ h ) \to \exists a \subseteq h: a=\{a\}$




**Replacement:** $\varphi(a,b) \land \varphi (a,c) \to b=c \\ \varphi(a,b) \to \operatorname{atom}(a) \land \exists l: l=\{b\} \\ A = \mathcal S \, a: \exists b \, (\varphi(a,b)) \\ B= \mathcal S \, b: \exists a \, \exists c \, ( \varphi(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?

This question is related to the question "[Is ZFGC, minimally modified to allow two Quine atoms instead of the empty set, synonymous\bi-interpretable with ZFGC?][1]", and I was hoping that the positive [answer][2] to it can be extended to the case here.


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


  [1]: https://mathoverflow.net/q/462747/95347
  [2]: https://mathoverflow.net/a/462761/95347