let G2 be _Graph; :: thesis:
let v1, v2 be Vertex of G2; :: thesis:
let e be object ; :: thesis:
let G1 be addEdge of G2,v1,e,v2; :: thesis:
assume that
A1: G2 is non-Dmulti and
A2: for e3 being object holds not e3 DJoins v1,v2,G2 ; :: thesis:

per cases ;

suppose A3: ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis:

for e1, e2, w1, w2 being object st e1 DJoins w1,w2,G1 & e2 DJoins w1,w2,G1 holds
e1 = e2

proof

let e1, e2, w1, w2 be object ; :: thesis:
assume that
A4: e1 DJoins w1,w2,G1 and
A5: e2 DJoins w1,w2,G1 ; :: thesis:
A6: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A3, Def11;

per cases by A4, Th75;

suppose A7: e1 DJoins w1,w2,G2 ; :: thesis:

per cases by A5, Th75;

suppose e2 DJoins w1,w2,G2 ; :: thesis:

hence e1 = e2 by A7, A1, GLIB_000:def 21; :: thesis:

end;

suppose A8: not e2 in the_Edges_of G2 ; :: thesis:

e2 in the_Edges_of G1 by A5, GLIB_000:def 14;
then e2 in {e} by A8, A6, XBOOLE_0:def 3;
then e2 = e by TARSKI:def 1;
then e2 DJoins v1,v2,G1 by A8, Th109;
then ( (the_Source_of G1) . e2 = v1 & (the_Target_of G1) . e2 = v2 ) by GLIB_000:def 14;
then ( v1 = w1 & v2 = w2 ) by A5, GLIB_000:def 14;
hence e1 = e2 by A2, A7; :: thesis:

end;

end;

end;

suppose A10: not e1 in the_Edges_of G2 ; :: thesis:

e1 in the_Edges_of G1 by A4, GLIB_000:def 14;
then e1 in {e} by A10, A6, XBOOLE_0:def 3;
then A11: e1 = e by TARSKI:def 1;

per cases by A5, Th75;

suppose A12: e2 DJoins w1,w2,G2 ; :: thesis:

e1 DJoins v1,v2,G1 by A10, A11, Th109;
then ( (the_Source_of G1) . e1 = v1 & (the_Target_of G1) . e1 = v2 ) by GLIB_000:def 14;
then ( v1 = w1 & v2 = w2 ) by A4, GLIB_000:def 14;
hence e1 = e2 by A2, A12; :: thesis:

end;

suppose A13: not e2 in the_Edges_of G2 ; :: thesis:

e2 in the_Edges_of G1 by A5, GLIB_000:def 14;
then e2 in {e} by A13, A6, XBOOLE_0:def 3;
hence e1 = e2 by A11, TARSKI:def 1; :: thesis:

end;

end;

end;

end;

end;

hence G1 is non-Dmulti by GLIB_000:def 21; :: thesis:

end;

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

then G1 == G2 by Def11;
hence G1 is non-Dmulti by A1, GLIB_000:89; :: thesis:

end;

end;