About Supergraphs. Part II

Abstract

In the previous article [5] supergraphs and several specializations to formalize the process of drawing graphs were introduced. In this paper another such operation is formalized in Mizar [1], [2]: drawing a vertex and then immediately drawing edges connecting this vertex with a subset of the other vertices of the graph. In case the new vertex is joined with all vertices of a given graph G, this is known as the join of G and the trivial loopless graph K1. While the join of two graphs is known and found in standard literature (like [9], [4], [8] and [3]), the operation discribed in this article is not.Alongside the new operation a mode to reverse the directions of a subset of the edges of a graph is introduced. When all edge directions of a graph are reversed, this is commonly known as the converse of a (directed) graph.