5.4 Declaration of Mode During a Demonstration

Many times, we declare mode variables during demonstrations. We will again enter a skeleton of a demonstration; for example, in the demonstration of P ⊆ Q:

      P c=　Q
       proof
        let x be set;
        assume x in P;
        ......
        thus x in Q;
       end;


At this point, it is stated as let x be set;.

       be mode name

With the above, we can declare mode during a demonstration. Of course, we can also state reserve x for set before hand.