4.4 Demonstration of the Equivalence

Concerning the demonstrating method for p iff q (p <=> q), p implies q is demonstrated first, then q implies p is demonstrated. The system automatically interprets p iff q as p implies q & q implies p. Therefore, if we state that p implies q, the first half is considered to be demonstrated. The rest is the other half's demonstration. As a result, with assume q, it becomes thus p and it is judged that p iff q is said.



  p iff q
    


   proof
     


    assume p;



     ...
     


    thus q;   p => q could be said



    assume q;



     ...
       


    thus p;   q => p can be said and p <=> q



   end;