3.2.4　Definitions Section

In the definitions section, when we want definition extension and expansion possible, we write file names of articles that have their definitions. For instance, when demonstrating X c= Y, we just need to demonstrate ∀a(a in X implies a in Y); however, this definition is defined in the article TARSKI as below.

   pred X c= Y means　x in X implies x in Y;

Therefore, if we write TARSKI in the definitions section, when we demonstrate X c= Y, it means that we demonstrated X c= Y if we can say that a in X implies a in Y.


Example,

       theorem X c=X \/ Y
           proof let x be set;
                assume　　x in X;
                hence y in X \/ Y by BOOLE:def 2;
           end: