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.