The constructor system of the Mizar proof checking system is explained here on examples from Mizar articles,and its translation
to untyped first-order syntax is described and discussed.This makes the currently largest library of formalized mathematics
available to first- order theorem provers.
A more detailed version of this article will be a part of author’s PhD thesis.