We add to Atomic General Extensional Mereology without Bottom, a primitive partial unary function symbol $\frak L$ denoting is the lable of. Then axiomatize:
**Axioms about the labeling function:**
- $\mathfrak L(x) = \mathfrak L(y) \to x=y$
- $\mathfrak L(x)=y \to \operatorname {atom}(y)$
- $\exists! x: \operatorname {atom}(x) \land \neg \exists y: x = \mathfrak L(y)$
***Define:*** $x \ \varepsilon \ y \iff x \ P \ y \land \operatorname {atom}(x) \\ x \in y \iff \exists z: y=\mathfrak L(z) \land x \ \varepsilon \ z$
From the above we get the important related theorems about mereologic totalities which we'll call them here "classes". That of
- Classes having the same $\varepsilon$-elements are equal
- Any class has an $\varepsilon$-element
- An $\varepsilon$-element $x$ of a class, is a class having $x$ as its sole $\varepsilon$-element.
- For any formula $\phi$ not using the symbol $x$ that holds of at least one $\varepsilon$-singleton class, there is a class $x$ whose $\varepsilon$ elements are the $\varepsilon$-singleton classes that satisfy $\phi$. We denote such $x$ by $[y \mid \phi(y)]$
We define "set" as an atom. While a "class" is any object of this theory! We reserve the notation $x=\{y \mid \phi(y)\}$ to mean $x$ is the label of the class $[y \mid \phi(y)]$ and if nothing fulfills $\phi$ then $x$ is the unique non-labeling atom.
The above system to be named as Labeled-Mereology, and it can be thought of being the background logic for the current development aiming to define set-membership and prove set theory axioms about it:
**The set axioms:**
- **Foundation:** $\not \exists x: \forall y \ \varepsilon \ x \exists z \ \varepsilon \ x \, (z \in y)$
Define: $\operatorname {Nice}(x) \iff \forall y \ P \ x \, \exists k: k=\mathfrak L(y) \\ \operatorname {nice}(x) \iff \forall y: x=\mathfrak L(y) \to \operatorname {Nice}(y) \\ \operatorname {nice}(F) \iff \operatorname {nice} (\operatorname {dom}(F)) $
In English: a class is Nice if and only if every part of it is labeled. A set is nice if and only if whatever it labels is a Nice class. A nice function is a function whose domain is a nice set.
- **Reflection:** if formula $\varphi(y,x_1,..,x_n)$ only uses $\in, =$ as predicates; then: $$\forall \operatorname {nice} x_1,..,x_n: \\ \forall y \, [ \varphi(y,x_1,..,x_n) \to \operatorname {nice}(y)] \to \\ \operatorname {Nice}([y \mid \varphi(y,x_1,..,x_n)])$$
- **Choice:** written in the usual manner.
This, I believe, would interpret $\sf ZFC$ in a manner analogous to Ackermann's over the realm of all $\in$-hereditarily nice sets. If we allow nice functions to be used among the parameters of Reflection, then we get to prove the existence of an $\in$-hereditarily nice set of all $\in$-hereditarily accessible sets, which is a model of $\sf ZFC$, thereby proving the consistency of set theory.