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];
          let y
          assume Q[y];
          thus R[y];

    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