4.7.2　given の使い方

　それから,ちょっと変わったスケルトンがあります．

　　　(ex x st P[x]) implies for y st Q[y] holds R[y]
　　　 proof
　　　　given x such that P[x];
　　　　······
　　　　······
　　　　let y
　　　　assume Q[y];
　　　　······
　　　　······
　　　　thus R[y];
　　　 end;


　この中で2行目の given x such that P[x] ; の given は assume と　consider を合わせた働きがあるわけです．

　　given = assume　+ consider

と覚えてください．こちらの方が簡単です．