4.6.4　文の分割 assume での場合

　such that 後の書き方の違いですが，これと似たことは assume の場合にも起こります．
例えば assume の例に，& S[x, y] を加えて，

　　　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;


と，なったとします．
　このとき，

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


は，

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


と書くこともできます．後の書き方に限って，P[x, y]とS[x, y]の両方にそれぞれにラベルを書くことができます．この例ではL1, L2というラベルです．