Also, in case of citing a definition, we write a name of an article : def a number.
Moreover, for proof ~ end, instead of the citation section, we can add a demonstration with some sentences like the following.
L3: A=C
proof
...
...
hence thesis;
end;
In this case, all of these are considered as one sentence. At this point, end in proof ~ end needs thus or hence just before it. It means that this can be said about the first formula that has a demonstration attached currently by this sentence's formula. Concerning the difference between thus and hence: hence takes the form of then + thus.
Even though then has appeared here for the first time, it is used when a formula stated before is cited. To explain with an example, let us assume the following.
L1:A=B by ...;
L2:B=C by ...;
At this point, instead of writing the following, because L2 formula is a formula stated before, we will take L2 away from the citation section of L3 sentence.
L3:A=C by L1,L2;
By using then, we can write the following.
then L3:A=C by L1;
The reason why we use then is because we want to minimize the usage of labels. Normally with demonstrations, we often cite formulas stated before. Also, when citing formulas from the one stated before, we will need many labels if we attach labels and state by label. However, by using then here, we will not need to use labels when citing formulas from the one stated before. Therefore, we can reduce the number of labels. Thus, when we want to cite formulas from the one stated before, even though it is not wrong to write by using labels, it is better to use then.
In addition, when checking with a checker (explained in Chapter 8.1.1) for improving an article used for registering in the Mizar library, everything will return an error if we write with the method of using the above labels even though the demonstrations are right. As long as that error exists, it will not be possible to register in the Mizar library. Therefore, it should not be written. Where then can be used, it should be used instead of labels. Because of this, hence should be used for citing formulas just before the end of proof ~ end.
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 environment 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.