4.6 All Symbols

We will now discuss about a predicate proposition. Let us demonstrate for x holds p[x] & q[x]. Further, p[x] means a predicate that includes x and it does not mean that brackets are permitted.

     for x holds P[x] & Q[x]
       proof
        let x;
         ······
         ······
        thus P[x]:
         ······
        thus Q[x]; (thesis)
       end:

    The word let exists as an opposite of for from all symbols. P is demonstrated by thus P[x] with leaving let x as it is. Further, we will demonstrate Q with Q[x].
    If it does not get confused, this letter can be changed. For example, the letter can be changed to y.