4.2 背理法
また同じことを証明するに，こういうやり方もあります．p implies q を証明したいときに，
p implies q
proof
assume p;
assume not q;
......
......
thus contradiction;
end;
proof中で，条件を仮定して assume p ，そして結論を否定します.
assume not q ．そうして，これから導いて thus contradiction
（矛盾）． これは背理法を使ったことになります．p でかつ q でないと仮定したら矛盾が生じたということになります．