Proof of A Term of One Type Whose Values Lie in a Class B Is a Term of Type B

We check the two conditions of Terms and Typed Terms under a Guard (ii) for the class $B$.

Condition Terms and Typed Terms under a Guard (iii): take an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$. Since $t$ is of type $A$ under $\gamma$, the same condition for $A$ shows that the value of $t$ under this assignment is a set, and by the hypothesis of (i) this value lies in $B$.

Condition Terms and Typed Terms under a Guard (iv) does not mention the type: it asks that, for every set variable $z$ that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $t$, the condition $\gamma\wedge z=t$ on $x_{1},\dots,x_{k}$ and $z$ be expressed by a predicative formula. This is literally the requirement that the same condition imposes for $A$, and it holds because $t$ is of type $A$ under $\gamma$.

Both conditions hold for $B$, so $t$ is a term of type $B$ under $\gamma$.