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.