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]
    let xs,y such that L:P[x,y];
    thus Q[x,y];

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.