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]
given x such that P[x];
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