4.6.2　such that を使った書き方

　それから，もう1つの書き方として次のようなものがあります．

　　　for x,y st P[x,y] holds Q[x,y]
　　　 proof
　　　　let xs,y such that L:P[x,y];
　　　　 ······
　　　　 ······
　　　　 ······
　　　　thus Q[x,y];
　　　 end;


　なお，such that のあとに，ふつうはラベルを入れます(この例の場合 L )．そして，最初の行のは st で，3行目は such that です．