  The observant reader will have spotted the appearance above of the expression weakly stratified. What is this? The instance of the comprehension that says that \(x \cup \{y\}\) always exists is stratified, and is therefore an axiom. So \(x \cup \{y\}\) always exists. So \(x \cup \{x\}\) always exists, by substitution. However the instance of the comprehension scheme alleging its existence is not stratified. The term ‘\(x \cup \{x\}\)’ is said to be weakly stratified by which it is meant that it can be stratified if we are allowed to give different types to distinct occurrences of free variables. Weak stratification is what is needed to admit ab initio those instances of the comprehension scheme that give us substitution instances of stratified instances, and not require a detour such as the detour here through the existence of \(x \cup \{y\}\).