4.4 同値の証明
次に，p iff q (p ⇔ q) の証明の仕方ですが，これは p implies q を証明し，それから q implies p を証明します．p iff q は，p implies q & 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;