let G2 be _Graph; for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is non-Dmulti & ( for e3 being object holds not e3 DJoins v1,v2,G2 ) holds
G1 is non-Dmulti
let v1, v2 be Vertex of G2; for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is non-Dmulti & ( for e3 being object holds not e3 DJoins v1,v2,G2 ) holds
G1 is non-Dmulti
let e be object ; for G1 being addEdge of G2,v1,e,v2 st G2 is non-Dmulti & ( for e3 being object holds not e3 DJoins v1,v2,G2 ) holds
G1 is non-Dmulti
let G1 be addEdge of G2,v1,e,v2; ( G2 is non-Dmulti & ( for e3 being object holds not e3 DJoins v1,v2,G2 ) implies G1 is non-Dmulti )
assume that
A1:
G2 is non-Dmulti
and
A2:
for e3 being object holds not e3 DJoins v1,v2,G2
; G1 is non-Dmulti
per cases
( ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 )
;
suppose A3:
(
v1 in the_Vertices_of G2 &
v2 in the_Vertices_of G2 & not
e in the_Edges_of G2 )
;
G1 is non-Dmulti
for
e1,
e2,
w1,
w2 being
object st
e1 DJoins w1,
w2,
G1 &
e2 DJoins w1,
w2,
G1 holds
e1 = e2
proof
let e1,
e2,
w1,
w2 be
object ;
( e1 DJoins w1,w2,G1 & e2 DJoins w1,w2,G1 implies e1 = e2 )
assume that A4:
e1 DJoins w1,
w2,
G1
and A5:
e2 DJoins w1,
w2,
G1
;
e1 = e2
A6:
the_Edges_of G1 = (the_Edges_of G2) \/ {e}
by A3, Def11;
end; hence
G1 is
non-Dmulti
by GLIB_000:def 21;
verum end; end;