This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.
In this article the finiteness of graphs is refined and the minimal and maximal degree of graphs are formalized in the Mizar system [3], based on the formalization of graphs in [4].