The Forster definition of well foundedness, which is essentially nothing but stratified $\in$-induction, i.e. a set $x$ is Forster well-founded if for any stratified property $P$ such that for any set $s$ if all elements of $s$ meet $P$ then $s$ must meet $P$ also, then $x$ must meet $P$. Now, the Sheridan definition of well foundedness (the last definition in the head post) is the dual of Forster's. 

First direction: if $x$ is Forster well-founded, then $x$ must be Sheridan well-founded

Proof: let $x$ be Forster well-founded and Sheridan non-well-founded, then there is a descending membership set $d$ where $x \in d$, now take the complementary set $d'$ of $d$, so $d'$ would be a superset of its own powerset, but $x$ is not in $d'$, contradicting it being Forster well-founded.

Second direction: if $x$ is Sheridan well-Founded, then $x$ is Forster well-founded

Proof: let $x$ be Sheridan well-founded but not Forster well-founded, so there must be a set $K$ such that $\mathcal P(K) \subseteq K$ and $x \notin K$. Now take the complementary set $K'$ of $K$, and $K'$ would be a descending membership set where $x \in K'$, contradicting $x$ being Sheridan well-founded.

Regarding the stance from the traditional definition (the second one in the head post), we have each traditional well-founded set being Sheridan well-founded, but not necessarily the converse.

Proof: if $x$ is traditional well founded and not Sheridan well-founded, then there is a descending membership set $d$ with $x \in d$. Now, $d \cap \operatorname {trcl}(x)$ would be a subset of the transitive closure of $x$ that is a descending membership set, violating the definition of traditional well-foundedness.

$\sf NFU$ cannot prove the other direction, since it doesn't prove existence of transitive closures for all sets. The problem with $\sf NFU$ is that possessing a transitive closure is not stratified. So, unlike in extensions of $\sf Zermelo$, it won't be guaranteed by $\in$-induction over all Forster (Sheridan) sets. So, $\sf NFU$ by itself won't grant the second direction, and so equivalence of the traditional definition with Forster (Sheridan) definition won't be proved. 

However, in the system presented in the head posting which uses Forster's definition, this would prove the existence of a transitive closure for every Forster well-founded set and hereditarily so, as well as $\in$-induction over Forster's well-founded sets for all formulas, and so would prove the equivalence with the traditional definition. But, if the theory in the head post was formalized in terms of the traditional definition, then it won't grant that equivalence.