Abstract
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.