let G be GraphUnion of G1,G2; :: thesis: G is non-Dmulti
the_Edges_of G1 misses the_Edges_of G2 by GLIB_012:80;
then A1: G1 tolerates G2 by Th12;

now :: thesis: for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G implies b₁ = b₂ )
assume A2: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ; :: thesis: b₁ = b₂
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_012:80;
then the_Vertices_of G1 = (the_Vertices_of G1) \/ (the_Vertices_of G2) ;
then A3: the_Vertices_of G = the_Vertices_of G1 by A1, Th25;
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) by A2, GLIB_000:16;
then A4: ( v1 in the_Vertices_of G1 & v2 in the_Vertices_of G1 ) by A3, GLIB_000:13;
A5: the_Edges_of G = (the_Edges_of G1) \/ (the_Edges_of G2) by A1, Th25;

per cases ( e1 DJoins v1,v2,G1 or not e1 DJoins v1,v2,G1 ) ;

suppose A6: e1 DJoins v1,v2,G1 ; :: thesis: b₁ = b₂

e2 DJoins v1,v2,G1

proof

assume not e2 DJoins v1,v2,G1 ; :: thesis: contradiction
then A7: not e2 in the_Edges_of G1 by A2, GLIB_006:71;
e2 in the_Edges_of G by A2, GLIB_000:def 14;
then A8: e2 in the_Edges_of G2 by A5, A7, XBOOLE_0:def 3;
G is Supergraph of G2 by A1, Th26;
then e2 DJoins v1,v2,G2 by A2, A8, GLIB_006:71;
hence contradiction by A6, GLIB_012:81; :: thesis: verum

end;

hence e1 = e2 by A6, GLIB_000:def 21; :: thesis: verum

end;

suppose not e1 DJoins v1,v2,G1 ; :: thesis: b₁ = b₂

then A9: not e1 in the_Edges_of G1 by A2, GLIB_006:71;
A10: G is Supergraph of G2 by A1, Th26;
e1 in the_Edges_of G by A2, GLIB_000:def 14;
then e1 in the_Edges_of G2 by A5, A9, XBOOLE_0:def 3;
then A11: e1 DJoins v1,v2,G2 by A2, A10, GLIB_006:71;
then v1 <> v2 by GLIB_000:136;
then not e2 DJoins v1,v2,G1 by A4, A11, GLIB_012:80;
then A12: not e2 in the_Edges_of G1 by A2, GLIB_006:71;
e2 in the_Edges_of G by A2, GLIB_000:def 14;
then e2 in the_Edges_of G2 by A5, A12, XBOOLE_0:def 3;
then e2 DJoins v1,v2,G2 by A2, A10, GLIB_006:71;
hence e1 = e2 by A11, GLIB_000:def 21; :: thesis: verum

end;

end;

end;

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