Consider the following premises. p_1 -> U(a_10). forall z: U(z) -> T(z). T(a_10) -> p_1. Can we infer p_1 <-> T(a_10) from them?
 From forall z: U(z) -> T(z) we can infer U(a_10) -> T(a_10). From p_1 -> U(a_10), U(a_10) -> T(a_10) we can infer p_1 -> T(a_10). Finally, from p_1 -> T(a_10), T(a_10) -> p_1 we can infer p_1 <-> T(a_10). Therefore, the answer is yes.