 Clause (3) in the two definitions supports the intention that \(\lambda\) binds variables (ensures that they are not free). Note the difference between \(\mathbf{BV}\) and \(\mathbf{FV}\) for variables.