let G1 be addAdjVertex of G,v1,e,v2; :: thesis:

per cases ;

suppose A1: ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis:

consider G3 being addVertex of G,v2 such that
A2: G1 is addEdge of G3,v1,e,v2 by A1, Th129;
reconsider w1 = v1 as Vertex of G3 by A1, Th72;
reconsider w2 = v2 as Vertex of G3 by Th98;
A3: for e1 being object holds not e1 DJoins w1,w2,G3

proof

w2 in {w2} by TARSKI:def 1;
then w2 in {w2} \ (the_Vertices_of G) by A1, XBOOLE_0:def 5;
then A4: w2 .edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that A5: e1 DJoins w1,w2,G3 ; :: thesis:
e1 Joins w2,w1,G3 by A5, GLIB_000:16;
hence contradiction by A4, GLIB_000:62; :: thesis:

end;

thus G1 is non-Dmulti by A2, A3, Th118; :: thesis:

end;

suppose A6: ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis:

consider G3 being addVertex of G,v1 such that
A7: G1 is addEdge of G3,v1,e,v2 by A6, Th130;
reconsider w2 = v2 as Vertex of G3 by A6, Th72;
reconsider w1 = v1 as Vertex of G3 by Th98;
A8: for e1 being object holds not e1 DJoins w1,w2,G3

proof

w1 in {w1} by TARSKI:def 1;
then w1 in {w1} \ (the_Vertices_of G) by A6, XBOOLE_0:def 5;
then A9: w1 .edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that A10: e1 DJoins w1,w2,G3 ; :: thesis:
e1 Joins w1,w2,G3 by A10, GLIB_000:16;
hence contradiction by A9, GLIB_000:62; :: thesis:

end;

thus G1 is non-Dmulti by A7, A8, Th118; :: thesis:

end;

suppose ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ; :: thesis:

then G1 == G by Def12;
hence G1 is non-Dmulti by GLIB_000:89; :: thesis:

end;

end;