4.7.1　consider の使い方

　take と逆の言葉として consider があります．

　　　(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;


となります．まず，assume します．assume ex x st P[x]; として，ここで consider を使って then consider a such that L:P[a] とします．この場合も such that がきますから，ラベルがないといけません．そして，こうしておいて，次に for y st . . . . . . を言うために let y such that Q[y] として thus Q[y] が言えればいいわけです．
　consider とは， P[x] を満たすような x が存在するとき，その存在する x に，なにか固有名詞を与えるという意味です．だから存在する x をいま1つ話題にしましょうということです．ですから，x でなくてもかまいません．a でもいいです．
　存在する a として，ここでは a が固有名詞のように使えるわけです．どこかに存在するとして使われているわけです．ですから consider は take の逆になります．take は固有名詞で何かにおけることに，存在記号をもって来ることに使います．