  Some illustrations may help: \(x \in x\) is not stratified. \(x \in y\) is. Thus not every substitution-instance of a stratified formula is stratified.  \(y = \wp(x)\) is stratified (the fancy P means power set), with the variable \(y\) being given a type one higher than the type given to \(x\). To check this we have to write out ‘\(y = \wp(x)\)’ in primitive notation. (In primitive notation, this formula becomes: \(\forall z(z \in y \leftrightarrow \forall w(w \in z \rightarrow w \in x))\). One can assign 0 to \(w, 1\) to \(z\), and 2 to \(x\), to get a stratification of this formula.) In general it is always necessary to write a formula out in primitive notation – at least until one gets the hang of it.