4.7.1 Method for Using Consider

Consider is an opposite word for take.

      (ex x st P[x]) implies for y st Q[y] holds R[y]
        proof
         assume ex x st P[x];
         then consider a such that L:P[a]
         ······
         ······
         let y such that Q[y];
         ······
         ······
         thus R[y];
        end;


First, we will assume. For assume ex x st P[x];, we use consider and state then consider a such that L:P[a]. This case also needs labels because such that exists. We will leave it like this and to state y st next, we will state let y such that Q[y] to state thus Q[y].
    Consider means to give some sort of proper nouns to an existing x that satisfies P[x]. Therefore, we intend to have an existing x as a topic for discussion. Thus, it does not have to be x, it can be a.
    As an existing a, it can be used as a proper noun here. In other words, it is used as if it is assumed to exist. Therefore, consider is an opposite of take. Take is used for replacing something as a proper noun or bring in existing symbols.