let G2 be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex e2, u1, u2 being object st
( e1 Joins u1,u2,G1 & e2 Joins u1,u2,G1 & e1 <> e2 )
take e ; :: thesis: ex u1, u2 being object st
( e1 Joins u1,u2,G1 & e Joins u1,u2,G1 & e1 <> e )
take v1 ; :: thesis: ex u2 being object st
( e1 Joins v1,u2,G1 & e Joins v1,u2,G1 & e1 <> e )
take v2 ; :: thesis: ( e1 Joins v1,v2,G1 & e Joins v1,v2,G1 & e1 <> e )
thus e1 Joins v1,v2,G1 by A3, Th74; :: thesis: ( 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; :: thesis: e1 <> e
thus e1 <> e by A1, A3, GLIB_000:def 13; :: thesis: verum

end;

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