3.3.2 Theorem

Generally, the main section is structured centering theorems and definitions.
    When writing a definition with an article, it should be written in the following way.

        theorem    a formula from the theorem
        proof
         ···
         ···
        end:


The difference between the method of writing the above and the below is that by writing a theorem, that formula is pulled out as an abstract file.

        Formula
        proof
         ···
         ···
        end:


An abstract file is a file that has a theorem, definition, and others that are pulled out of an article (.ABS file). When we register an article in the Mizar library, we change an article into an abstract file. The reason for this is because articles that contain everything such as demonstrations (.MIZ file) become too big, and it is hard to find anything for phrasing. Therefore, when we write formulas that we desire to be cited, we put in a theorem.
    When we write definitions with an article, we use a definition. Also, when some new words or functions are to be defined, this definition is used to define them. We will explain definitions later in more detail.
Further, a theorem or definition cannot be written in proof ∼ end. We can only use them in the top step of a nest. In short, we cannot write as follows.

      theorem　...
        proof
          theorem　...
            proof
            ···
            ···
            end;
        end;

    As explained, a Mizar article is largely divided into the environ section and the main section. The main section is usually structured with some definitions and theorems.
    Also, in a Mizar article, after :: is a comment.