let G be GraphUnion of G1,G2; G is non-Dmulti
the_Edges_of G1 misses the_Edges_of G2
by GLIB_012:def 6;
then A1:
G1 tolerates G2
by Th12;
now for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2let e1,
e2,
v1,
v2 be
object ;
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G implies b1 = b2 )assume A2:
(
e1 DJoins v1,
v2,
G &
e2 DJoins v1,
v2,
G )
;
b1 = b2
the_Vertices_of G1 = the_Vertices_of G2
by GLIB_012:def 6;
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
;
b1 = b2
e2 DJoins v1,
v2,
G1
proof
assume
not
e2 DJoins v1,
v2,
G1
;
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:46;
verum
end; hence
e1 = e2
by A6, GLIB_000:def 21;
verum end; suppose
not
e1 DJoins v1,
v2,
G1
;
b1 = b2then 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
not
e2 DJoins v1,
v2,
G1
by A4, GLIB_012:def 6;
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;
verum end; end;
hence
G is non-Dmulti
by GLIB_000:def 21; verum