Consider the proposition that \(m\) is an even number expressed as the formula \(\exists n \in {{\mathbb N}}. m= 2n\). We can build a set of proof-objects corresponding to this formula by using the general set-theoretic sum operation. Suppose that \(A_n\) (\(n\in {{\mathbb N}}\)) is a family of sets. Then its disjoint sum is given by the set of pairs