Foundation and the absence of descending membership sequences
= Foundation and the absence of descending membership sequences
<Foundation> implies that no <descending membership sequence> exists. Conversely, with <dependent choice>, failure of <foundation> gives a nonempty <set> in which every element contains another element of that <set>. Successively selecting such members produces a <descending membership sequence>. Thus the two conditions are equivalent with <dependent choice>; full <choice> is sufficient.