Miscellaneous graph preliminaries (Q2658808)

The impressive Mizar system is intended to support computer-aided proofs of mathematical results. Starting in the early 1970s, after evolving through several generations of development, especially since 1989, a knowledge base, Mizar Mathematical Library, has now been created that contains a collection of formalized knowledge of mathematics, \textit{Verifier}, a verification system, and other supporting components. New works, \textit{Mizar articles}, are prepared, expressed in the Mizar language, verified, submitted, reviewed, accepted, extracted, and finally, incorporated into this knowledge base, which currently includes more than 9,400 definitions, and more than 49,000 theorems. Readers are referred to [\textit{G. Bancerek} et al., J. Autom. Reasoning 61, No. 1--4, 9--32 (2018; Zbl 1433.68530)] for a full discussion of the background, development, current status, and future goals, of this exciting system, as well as to its official site \url{mizar.org} for many more details, including the affiliated journal, Formaliz. Math., where this article appears. This article suggests to add a collection of one hundred ``preliminaries'', or basic facts, mostly related to graph theory, when an edge is added to a graph to result in another graph. For example, Proposition 21 states that ``Let us consider a graph \(G\), a vertex \(v\) of \(G\), and objects \(e\), \(w\). If \(v\) is isolated, then \(e\) does not join \(v\) and \(w\) in \(G\).'' As another example, after stating that ``Let us consider a graph \(G\), a set \(V\), a supergraph \(H\) of \(G\) extended by the vertices from \(V\), and a subset \(E\) of the edges of \(G\)'', Proposition 75 states that ``\(E\) is a representative selection of the parallel edges of \(G\) if and only if \(E\) is a representative selection of the parallel edges of \(H\).'' It also contains twenty preliminaries not directly related to graphs at the beginning, where Proposition~1 states that: Let \(X\), \(Y\) and \(Z\) be sets, ``If \(Z \subseteq X\), then \(X \cup Y \setminus Z=X \cup Y\).'' This phrase of ``\(X \cup Y \setminus Z\)'' is clearly ambiguous. When \(X=\{1, 2\}\), \(Y=\{2\}\), and \(Z=\{1\}\), \((X \cup Y) \setminus Z \not =X \cup Y\). On the other hand, \(X \cup (Y \setminus Z)=X \cup Y\). I would rewrite ``\(X \cup Y \setminus Z\)'' as ``\(X \cup (Y \setminus Z)\)'' in Proposition 1.