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 Any;



    assume x C P ;
    


    ......
                         


    thus x C Q;



   end;

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



    be mode name

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

5.4.1 Warning About c=

Also, as a caution, we use c= for in Mizar. However, when using c= , we need to leave a space in front and back.

5.4.2 Example of Actually Using a Definition

Furthermore, here, we demonstrate (V x)(x C P => x C Q) and it does not mean that we demonstrated P Q. There is a mathematical distance between these two. However, the system understands the fact that both of them are equivalent by writing TARSKI in the definition of the environment section as explained in the third chapter. It means that this is defined as a predicate in the abstract file of TARSKI.

TARSKI is structured from the definition which is the basis of the Mizar library; therefore, when writing articles, we write TARSKI at the definition of the environment section.