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.