let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & ex e2 being object st e2 DJoins v1,v2,G2 holds
not G1 is non-Dmulti
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & ex e2 being object st e2 DJoins v1,v2,G2 holds
not G1 is non-Dmulti
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & ex e2 being object st e2 DJoins v1,v2,G2 holds
not G1 is non-Dmulti
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 & ex e2 being object st e2 DJoins v1,v2,G2 implies not G1 is non-Dmulti )
assume that
A1: not e in the_Edges_of G2 and
A2: ex e2 being object st e2 DJoins v1,v2,G2 ; :: thesis: not G1 is non-Dmulti
ex e1, e2, u1, u2 being object st
( e1 DJoins u1,u2,G1 & e2 DJoins u1,u2,G1 & e1 <> e2 )

proof

consider e2 being object such that
A3: e2 DJoins v1,v2,G2 by A2;
take e ; :: thesis: ex e2, u1, u2 being object st
( e DJoins u1,u2,G1 & e2 DJoins u1,u2,G1 & e <> e2 )
take e2 ; :: thesis: ex u1, u2 being object st
( e DJoins u1,u2,G1 & e2 DJoins u1,u2,G1 & e <> e2 )
take v1 ; :: thesis: ex u2 being object st
( e DJoins v1,u2,G1 & e2 DJoins v1,u2,G1 & e <> e2 )
take v2 ; :: thesis: ( e DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 & e <> e2 )
thus e DJoins v1,v2,G1 by A1, Th109; :: thesis: ( e2 DJoins v1,v2,G1 & e <> e2 )
thus e2 DJoins v1,v2,G1 by A3, Th74; :: thesis: e <> e2
thus e <> e2 by A1, A3, GLIB_000:def 14; :: thesis: verum

end;

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