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

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

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

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

suppose A5: e1 Joins v1,v2,G1 ; :: thesis: b₁ = b₂

e2 Joins v1,v2,G1

proof

assume not e2 Joins v1,v2,G1 ; :: thesis: contradiction
then A6: not e2 in the_Edges_of G1 by A2, GLIB_006:72;
e2 in the_Edges_of G by A2, GLIB_000:def 13;
then A7: e2 in the_Edges_of G2 by A4, A6, XBOOLE_0:def 3;
G is Supergraph of G2 by A1, Th26;
then e2 Joins v1,v2,G2 by A2, A7, GLIB_006:72;
hence contradiction by A5, GLIB_012:100; :: thesis: verum

end;

hence e1 = e2 by A5, GLIB_000:def 20; :: thesis: verum

end;

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

then A8: not e1 in the_Edges_of G1 by A2, GLIB_006:72;
A9: G is Supergraph of G2 by A1, Th26;
e1 in the_Edges_of G by A2, GLIB_000:def 13;
then e1 in the_Edges_of G2 by A4, A8, XBOOLE_0:def 3;
then A10: e1 Joins v1,v2,G2 by A2, A9, GLIB_006:72;
then v1 <> v2 by GLIB_000:18;
then not e2 Joins v1,v2,G1 by A3, A10, GLIB_012:98;
then A11: not e2 in the_Edges_of G1 by A2, GLIB_006:72;
e2 in the_Edges_of G by A2, GLIB_000:def 13;
then e2 in the_Edges_of G2 by A4, A11, XBOOLE_0:def 3;
then e2 Joins v1,v2,G2 by A2, A9, GLIB_006:72;
hence e1 = e2 by A10, GLIB_000:def 20; :: thesis: verum

end;

end;

end;

hence G is non-multi by GLIB_000:def 20; :: thesis: verum