4.6.5　that の後の注意

　that の使い方についていいますと，that の後には then を使うことができません．どうしてかというと，such that の後に2つ以上の文があるかもしれないと考えるからです．2つ以上の文がある場合は，直前の文というのがはっきりしません．ですから，

　　　　assume that A and B:
　　　　then C;


こういう書き方はできません．必ずラベルを使って，

　　　　assume that L1:A and L2:B;
　　　　C by L1,L2;


こういうふうに書かないといけません．あるいは，B だけ使うときは，

　　　　C by L2;


これだけ書きます．引用が1つの場合にも then は使えません．then でなく by L2 と書かなければいけません．ですから that が来たらラベルが来なければこの文は使えません．that の後には必ずラベルが来ると考えられます．
　that をつけなければ then を使えます．ですから，最初の書き方，
assume P[x, y] & Q[x, y]の場合は，

　　　assume P[x,y] & Q[x,y];
　　　then　......


と使うことができます．that がなくて，1つの文しかないわけです．assume のときは then を使います．