 where \(\bar{X}\)is a sequence of higher-order variables and \(\bar{t}\) a corresponding instantiation. So, \(\bar{t}\) designates some sequence of relations and functions that satisfies TC in the context of an antecedently given interpretation of \(V_o\). Once such a sequence has been defined via the epsilon-operator, the second step of the definition is straightforward: