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