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: