4.4　同値の証明

　次に　p iff q (p ⇔ q)の証明の仕方ですが，これは　p implies qを証明し，それから q implies p を証明します．p iff q は，p implies q　&amp　q implies p とシステムは自動的に解釈します．ですから，p implies q をいいますと，前半は証明したことになります．あとは後半の証明だけです．そうして　assume q で，thus p となったので，これで　p iff q がいえたと判断するわけです．

　　p iff q
　　 proof
　　　assume p;
　　　···
　　　thus q;　　p ⇒ q がいえた
　　　assume q;
　　　···
　　　thus p;　　q ⇒ p がいえて p ⇔ q
　　end: