How do I interpret the wording of this passage about abstract binding trees from the book Practical Foundations of Programming Languages
Just to clear something up that may not have been obvious, $\chi$ is a set and the notation $B[\chi, x]$ is meant to be ABTs under free variables that are either $x$ or are in $\chi$. In this notation I believe it is implied that $x \notin \chi$ when you write $B[\chi, x]$, which is important.

Using the definition of ABT above, you cannot prove for any $\chi$ that let(z, x.x) is in $B[\chi,x]$, but i claim that this is necessary to prove if you want to use it as the inner formula $a_1$ in let(y, x.$a_1$).

The reason you cannot prove let(z, x.x) is in $B[\chi,x]$ is because using the rule#1 stated above, the free variable $x$ is only an ABT in $B[\chi]$ when $x \in \chi$ (or alternatively: $x$ is only an ABT in $B[\chi',x]$ for some $\chi'$), but then using rule#2, we deduce $z \in B[\chi] \wedge x \in B[\chi, x] \rightarrow let[z,x.x] \in B[\chi]$. As I had mentioned in the first paragraph, this implies $x \notin \chi$, which means that the formula let(z, x.x) is ONLY in ABTs where $x$ is not a free variable.

The reason why $x$ needs to be free in this inner formula is because otherwise we cant apply rule#2 again on the outer formula let(y, x.$a_1$).