4.7　存在記号

　さらにいろいろなスケルトンがあります．存在記号を含んだ述語論理式 ex x st P[x] の証明のしかたですが，この場合 take というものを使います．
　takeを使って，

　　　　ex x st P[x]
　　　　　proof
　　　　　------
　　　　　L:P[a];
　　　　　take a:
　　　　　thus thesis by L;
　　　　 end;


と書きます．P[x]を満たす x が存在することを証明するときに，P[a]が証明されたとします．すると take a として，存在する x として，a を取ってくれば，L による証明をされたことになります．