References

As was stated in [3] we publish mathematical papers which are abstracts of Mizar articles to be found in the Main Mizar Library (MML). An article includes certain elements which are transferred to the data base, such as theorems or definitions. This has been due to the fact that the material published there was at first intended to help the Mizar users to handle the data base. Thus the works published there describe the present state of MML and are, in a sense, a report on the expansion of that library. Next to them there are also new mathematical papers because the new method of formalization is not trivial even though it refers to simple mathematical facts. It must be explained at this point that both the PC-Mizar verifier and MML are being systematically developed. In the case of PC-Mizar it is mainly the Mizar language which is enriched, which makes it more convenient to write articles; the same might be said of proof-checker, which enables one to write shorter proofs and articles. The development of MML consists in continuous revisions of articles accepte