4.6.4 Dividing Sentences With Assume

For the difference in writing a method after such that, a similar thing occurs in the case of assume. For example, adding & S[x,y] to an assume example, we will assume that the following occurred.

     for x,y st P[x,y] & S[x,y] holds Q[x,y]
       proof
        let x,y;
        assume P[x,y] & S[x,y];
        ······
        ······
        thus Q[x,y];
       end;


    At this point,

      assume P[x,y] & S[x,y];


can be written as below.

      assume that L1:P[x,y] and L2:S[x,y];


Only with the way of writing the above formula, we can write labels on both P[x,y] and S[x,y]. In this example, they are L1 and L2 labels.