Lets see how the world of sets could look like from the perspective of $\sf NFU$. So, here we work within the first order language of set theory, with the following extra-logical axioms:

**1. **Quine atom:****  There exists a unique Quine atom, i.e. a singleton that is an element of itself.

An "*urelement*" is defined as a singleton of the Quine atom. That is, it has one element and that element is the Quine atom.

**2. Extensionality:** if  $x$ is not an urelement, then every set co-extensional with $x$ is equal to $x$. 

**3. Stratified Comprehension:** as stated in $\sf NFU$.


**4. Urelements:** The set of all urelements is bijective with the set of all objects, i.e. the set of all urelements is as big as the universe.

**5. Choice:** as stated in $\sf NFU$.

***Define:*** a set is said to be well founded if it is an element of every set that is a superset of its own powerset. Formally:

 $$\operatorname {well-founded}(s) \iff  \forall X: \mathcal P(X) \subseteq X \to s \in X$$

 

**6. Replacement:** if $A$ is a well founded set, and $\phi(x,y)$ is a formula standing for a many-to-one relation from well founded sets to well founded sets, then there is a set $\{y \mid \exists x \in A : \phi(x,y)\}$.

**7. Infinity:** There is a well-founded set having the empty set among its elements, that is closed under singletons.

So, this theory has a universe obeying the rules of $\sf NFU$ (but with urelements being the singletons of the Quine atom, instead of the usual formulation as element-less objects), and that has its well founded realm obeying the rules of $\sf ZFC$. 

The definition of well-foundedness is due to Thomas Forster, while the theory is speaking about Holmes's $\sf BEST$ model of $\sf NFU$ with little modification.

This theory is way stronger than $\sf ZFC$ and of course $\sf NFU$, it goes high up to measurable cardinals. 

Now, my question is about that definition of well foundedness which is just a recapture of stratified $\in$-induction in $\sf NFU$ terms. How this compares to the traditional definition of well foudedness: 

\begin{align} \operatorname {well-founded}(s) \iff  \exists t : \ & \operatorname {trs}(t) \land s \subseteq t \ \land \\&\forall v: \operatorname {trs}(v) \land s \subseteq v \to t \subseteq v \ \land \\ & \forall c \subseteq t \exists b \in c: b \cap c = \varnothing \end{align}

This definition also obeys stratified $\in$-induction.