5.4.2 Example of Actually Using a Definition
Furthermore, here, we demonstrate and it does not mean that we demonstrated . 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 definitions of the environ 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 definitions of the environ section.