4.7.2 Method for Using Given

There is another skeleton that is slightly different.

(ex x st P[x]) implies for y st Q[y] holds R[y]

proof

given x such that P[x];

······

······

let y

assume Q[y];

······

······

thus R[y];

end;

Here, given in the second sentence: "given x such that
P[x];", works as both assume and consider.

Please remember as follows. It is much easier.

given = assumeă€€+ consider