Rank bounding for sets in the cumulative hierarchy (source code)

= Rank bounding for sets in the cumulative hierarchy
{title2=$a\subseteq V\Longrightarrow a\in V$}

If every member of a <set> $a$ belongs to some cumulative-hierarchy stage, <replacement> collects the least such stages. Their <ordinal> <supremum> gives a common stage $V_\beta$ containing every element of $a$, so $a\in V_{\beta+1}$. The argument also works without <foundation> and bounds a <set> of well-founded elements inside the hierarchy.