Consider the following premises. t -> T_3(c_4). W(c_4) <-> t. forall z_1: T_3(z_1) -> W(z_1). Can we infer W(c_4) -> T_3(c_4) from them?
 From forall z_1: T_3(z_1) -> W(z_1) we can infer T_3(c_4) -> W(c_4). From W(c_4) <-> t we can infer W(c_4) -> t. Finally, from W(c_4) -> t, t -> T_3(c_4) we can infer W(c_4) -> T_3(c_4). Therefore, the answer is yes.