let G2 be addVertices of G,V; G2 is non-Dmulti
for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 holds
e1 = e2
proof
let e1,
e2,
v1,
v2 be
object ;
( e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 implies e1 = e2 )
assume
(
e1 DJoins v1,
v2,
G2 &
e2 DJoins v1,
v2,
G2 )
;
e1 = e2
then
(
e1 DJoins v1,
v2,
G &
e2 DJoins v1,
v2,
G )
by Th89;
hence
e1 = e2
by GLIB_000:def 21;
verum
end;
hence
G2 is non-Dmulti
by GLIB_000:def 21; verum