There is a version of Mereology in which there is no Bottom atom, and yet it is synonymous with the above theory, and if I'm correct about the above theory $\sf M$ being synonymous with MK-Foundation-Choice, then that answers this question to the positive. The idea is to modify the underlying mereology as to have a kind of alien atom mereologically speaking, that is an object that doesn't overlap with any other object! This was done in a [prior][1] posting. Now, to enable that here, we need to adjust composition as to forbid composing objects using that atom. Now, we use this atom to be the non-labeling atom. Here is the exposition of it: **Language:** first order logic with equality, with primitives of $\subseteq$ standing for Part-hood, and $\{ * \}$ standing for the singleton function which is a partial unary function. The axioms are: ***Mereological Axioms:*** ***Define:*** $atom(X) \iff \forall Y \subseteq X \, (Y = X)$ ***M1*** $\textbf{Atomism: } \forall \ atom \ X \ ( X \subseteq Y \to X \subseteq Z) \leftrightarrow Y \subseteq Z$ ***Define:*** $ X \subsetneq Y \iff X \subseteq Y \land X \neq Y $ ***Define:*** $atom^*(X) \iff atom(X) \land \exists Y: X \subsetneq Y $ ***M2*** $\textbf{Extensionality: }\forall \ atom^* \ X \, (X \subseteq A \leftrightarrow X \subseteq B ) \to A=B$ ***Define:*** $X \ \mathcal O \ Y \iff \exists Z: Z \subseteq X \land Z \subseteq Y$ ***M3*** $\textbf{Alien: }\exists X \forall Y: Y \neq X \to \neg X \ \mathcal O \ Y$ ***Define:*** $X = \varnothing \iff \forall Y: Y \neq X \to \neg X \ \mathcal O \ Y$ ***M4*** $\textbf{Composition: } \exists X \forall \ atom^* \ Y \ ( Y \subseteq X \leftrightarrow \psi( Y )); \text{ if } X \text { is not free in } \psi $ ***Define:*** $X = \bigl[Y \mid \psi \bigr] \iff \forall \ atom^* \ Y \ ( Y \subseteq X \leftrightarrow \psi( Y )) $ ***Labeling Axioms*** ***L1*** $\textbf{Labeling: } \{X\}=\{Y\} \to X=Y$ ***L2*** $\textbf{Purity: } \exists X \ (\{X\} =Y) \leftrightarrow atom^*(Y) $ ***L3*** $\textbf{Replacement: } \text { if } \psi(X,Y) \text { is a formula, then: } \\ \forall X \neg \exists^{>1} Y: \psi(X,Y), \land \\ B= \bigl[ K \mid K \subseteq Y \land \exists V (V=\{Y\} \lor Y=\{V\}) \land \exists X \subseteq A \ :\psi(X,Y)\bigr] \land \\\exists Z: \{A\}=Z \\\to\\\exists Z: \{B\}=Z $ ***L4*** $\textbf{Infinity: } \exists I \exists X: \forall \ atom \ Y \subseteq X \bigl(\exists Z \subseteq X: Z=\{Y\} \bigr) \land \{X\}=I $ Now to interpret $\sf M$ in this theory, we take the domain to be all objects here, so there is no restriction, we keep the same equality relation, we re-define $P$ as $X \ P \ Y \equiv_{def} X \subseteq Y \lor X=\varnothing $ , and of course define $\mathfrak L$ as: $\mathfrak L(X)=Y \equiv_{def} Y = \{X\}$ For the opposite direction, we work in $\sf M$, keep the same domain, and equality relations, re-define $\subseteq$ as: $ X \subseteq Y \equiv_{def} X \ P \ Y \land X \neq \varnothing$ , and of course define the singleton function as: $\{X\}=Y \equiv_{def} \mathfrak L(X)=Y$ We'll use the equality relation as our needed i-isomorphisms in both directions. $\small \square$ As regards the system $\sf M-Bottom$ mentioned in the question, I think it is not bi-interpretable with MK-Foundation-Choice, since it would be haunted by the same argument present in a [prior posting][2]. [1]: https://mathoverflow.net/q/412970/95347 [2]: https://mathoverflow.net/a/459098/95347