This article formalizes different variants of the complement graph in the Mizar system [3], based on the formalization of graphs in [6].