4.7 Existing Symbols

There are more different kinds of skeletons. In the case of demonstrating
logical predicate formulas with existing symbols ex x st P[x], we use take.

By using take, we write the following:

ex x st P[x]

proof

------

L:P[a];

take a:

thus thesis by L;

end;

When demonstrating the existence of x that satisfies P[x], let us assume that P[a] is demonstrated. In this case, it means that for take a, x is exists and if we take a, it is demonstrated by L.