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.