4.6.2 Method for Writing With such that

In addition, there is another way of writing as follow:

　　　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;

Further, labels are usually entered after such that; however, in this example (this case L) they are not necessary. The first line is st and the third line is such that.