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 not e in the_Edges_of G2 & v1,v2 are_adjacent holds
not G1 is non-multi
let v1, v2 be Vertex of G2; for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v1,v2 are_adjacent holds
not G1 is non-multi
let e be object ; for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v1,v2 are_adjacent holds
not G1 is non-multi
let G1 be addEdge of G2,v1,e,v2; ( not e in the_Edges_of G2 & v1,v2 are_adjacent implies not G1 is non-multi )
assume that
A1:
not e in the_Edges_of G2
and
A2:
v1,v2 are_adjacent
; not G1 is non-multi
ex e1, e2, u1, u2 being object st
( e1 Joins u1,u2,G1 & e2 Joins u1,u2,G1 & e1 <> e2 )
proof
consider e1 being
object such that A3:
e1 Joins v1,
v2,
G2
by A2, CHORD:def 3;
take
e1
;
ex e2, u1, u2 being object st
( e1 Joins u1,u2,G1 & e2 Joins u1,u2,G1 & e1 <> e2 )
take
e
;
ex u1, u2 being object st
( e1 Joins u1,u2,G1 & e Joins u1,u2,G1 & e1 <> e )
take
v1
;
ex u2 being object st
( e1 Joins v1,u2,G1 & e Joins v1,u2,G1 & e1 <> e )
take
v2
;
( e1 Joins v1,v2,G1 & e Joins v1,v2,G1 & e1 <> e )
thus
e1 Joins v1,
v2,
G1
by A3, Th74;
( e Joins v1,v2,G1 & e1 <> e )
e DJoins v1,
v2,
G1
by A1, Th109;
hence
e Joins v1,
v2,
G1
by GLIB_000:16;
e1 <> e
thus
e1 <> e
by A1, A3, GLIB_000:def 13;
verum
end;
hence
not G1 is non-multi
by GLIB_000:def 20; verum