4.6.1　変数が2つある場合

　それから次の様に変数が2つある場合ですが，

　　　for x,y st P[x,y] holds Q[x,y]
　　　 proof
　　　　let x,y;
　　　　assume P[x,y];
　　　　 ······
　　　　 ······
　　　　thus Q[x,y]; (thesis)
　　　 end;


　このように変数を2つ書きます．直接的には， を証明したことになります．assume ....... は1つの論理式になっています．