Working in bi-sorted FOL, where lower cases stand for *sets* and upper cases for *classes*; add all axioms of ZF written completely in lower case, and add an axiom of Extensionality over all classes, and the following axioms: $\forall x \ \exists Y: Y=x$ $\forall X \ \forall Y: X \in Y \to \exists z: z=X$ $\forall \vec{Z} \ \exists X \ \forall y \ (y \in X \iff \phi(y, \vec{Z}))$; if $\phi(y, \vec{Z})$ is a formula not using $``X"$. Define $V$ as the class of all sets. Is there a clear inconsistency with the following principle? Define recursively: $J_0``x = J(x) \\ J_{n+1} `` x= \{J_n`` y \mid y \in x \}$ **Internalization schema:**$n=1,2,... \\ \forall \text { infinite } x,y \ \exists J \ ( J: x \rightarrowtail y \land \forall s: J_n ``s \in V )$