 Second epsilon theorem: Suppose \(\Gamma \cup \{A\}\) is a set of formulae not involving the epsilon symbol. If \(A\) is derivable from \(\Gamma\) in the epsilon calculus, then \(A\) is derivable from \(\Gamma\) in predicate logic.