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 (\exists \{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) \lor \exists l: l=\{a\} )\land (\operatorname{atom}(b) \lor \exists l: l=\{b\}) \\ A = \mathcal S \, a: \exists b\exists c \, ( \varphi(c,b) \land a \subseteq c ) \\ B= \mathcal S \, b: \exists a \, \exists c \, ( \varphi(a,c) \land b \subseteq c ) \\ \to \\ \exists l: l=\{A\} \to \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 \exists l: l=\{x\} \land \forall y: \{y\} \subseteq x \to \{\{y\}\} \subseteq x$

Choice: $\exists C \, \forall x \, \exists y : y=C(x) \land \exists \{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?", and I was hoping that the positive answer 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$". The expression "$\exists \{x\} \subseteq y$" stands for "$\exists z: z=\{x\} \land z \subseteq y$".