let G1 be addAdjVertex of G,v1,e,v2; :: thesis: G1 is non-multi

per cases ( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( ( 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 ) ) ) ;

suppose A1: ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G1 is non-multi

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;
for e1 being object holds not e1 Joins 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 A3: w2 .edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that A4: e1 Joins w1,w2,G3 ; :: thesis: contradiction
e1 Joins w2,w1,G3 by A4, GLIB_000:14;
hence contradiction by A3, GLIB_000:62; :: thesis: verum

end;

then A5: not w1,w2 are_adjacent by CHORD:def 3;
thus G1 is non-multi by A2, A5, Th120; :: thesis: verum

end;

suppose A6: ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G1 is non-multi

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;
for e1 being object holds not e1 Joins 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 A8: w1 .edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that A9: e1 Joins w1,w2,G3 ; :: thesis: contradiction
thus contradiction by A8, A9, GLIB_000:62; :: thesis: verum

end;

hence G1 is non-multi by A7, Th120, CHORD:def 3; :: thesis: verum

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: G1 is non-multi

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

end;

end;