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.