Caminati, M. B. Basic First-Order Model Theory in Mizar. JFR 2010, 3, 49-77.