Description: In a simple graph, there is no loop, i.e. no edge connecting a vertex
with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017)(Proof shortened by Alexander van der Vekens, 20-Mar-2018)(Revised by AV, 17-Oct-2020)(Proof shortened by AV, 11-Dec-2020)