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