4.6.1 When There Are Two Variables
When there are two variables like the following we write two variables.
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;
Directly, it means that we demonstrated . assume ..... becomes one logical formula.