A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed as such a graph. In this article, this correspondence is formalized in the Mizar system [2], based on the formalization of graphs in [6] and relations in [11], [12]. Notably, a new definition of createGraph will be given, taking only a non empty set