Consider the following premises. forall x_2: T(x_2) <-> S_2(x_2). Can we infer S_2(a_2) -> T(a_2) from them?
 From forall x_2: T(x_2) <-> S_2(x_2) we can infer T(a_2) <-> S_2(a_2). Finally, from T(a_2) <-> S_2(a_2) we can infer S_2(a_2) -> T(a_2). Therefore, the answer is yes.