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.