4.11　takeについて

　4.7節の繰り返しになりますが，take についてより詳しく説明します．

　　　　　　ex r bring Real st 1<r-1
　　　　　　　　　　　　　　　　-------(1)

を証明するとき，次のようにします．

　　theorem ex r being Real 1<r-1
　　proof 1+1<3;then A1:1+1-1<3-1 by REAL_1:59;
　　　　take　3;
　　　　thus 1く3-1 by REAL_2:17,A1;
　　end:

最終の式が(1)の形でなく

　　　　　　thus 1<3-1

となっていることに注意して下さい．これは途中に take 3 があるためで，これによって最終の式から存在記号の部分が取り除かれ，裸の部分だけを証明すればよいことになります．
　これをもう少し詳しく説明すると，

　　　　(∃x)(∃y)(f(x,y))を証明するのに，

　　　proof　 ------　------　この段階での証明すべき式は(∃x)(∃y)(f(x,y))
　　　　　　　　------ ------
　　　　　　　　take a　 ------　この段階での証明すべき式は(∃y)(f(a,y))
　　　　　　　　------ ------
　　　　　　　　take b　 ------　この段階での証明すべき式は(f(a,b))
　　　　　　　　------ ------
　　　　　　　　hence f(a.b);
　　　end;

だから次のような証明ができます．

　　theorem ex r,s being Real st 1<r-1
　　proof take 3;
　　　　take 1;1<3;
　　　　hence thesis by REAL_2:17;
　　end;

なお，take を使わなくても多くの場合，上の f(a,b) にあたる所を証明すれば，最終的にチェッカーが a と b を探してくれます．例えば，

　　theorem ex r being Real st 1<r-1
　　proof 1+1<3;then 1+1-1<3-1 by REAL_1:59; then
　　　　1<3-1 by REAL_2:17;
　　　　hence thesis;
　　end;

のようにしてもよいのです．