M. B. Caminati, “Basic first-order model theory in Mizar”, JFR, vol. 3, no. 1, pp. 49–77, Jan. 2010.