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 G2 is non-multi & not v1,v2 are_adjacent holds
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 G2 is non-multi & not v1,v2 are_adjacent holds
G1 is non-multi
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st G2 is non-multi & not v1,v2 are_adjacent holds
G1 is non-multi
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( G2 is non-multi & not v1,v2 are_adjacent implies G1 is non-multi )
assume that
A1: G2 is non-multi and
A2: not v1,v2 are_adjacent ; :: thesis: G1 is non-multi

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 ) ; :: thesis: G1 is non-multi

for e1, e2, w1, w2 being object st e1 Joins w1,w2,G1 & e2 Joins w1,w2,G1 holds
e1 = e2

proof

let e1, e2, w1, w2 be object ; :: thesis: ( e1 Joins w1,w2,G1 & e2 Joins w1,w2,G1 implies e1 = e2 )
assume that
A4: e1 Joins w1,w2,G1 and
A5: e2 Joins w1,w2,G1 ; :: thesis: e1 = e2
A6: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A3, Def11;

per cases ( e1 Joins w1,w2,G2 or not e1 in the_Edges_of G2 ) by A4, Th76;

suppose A7: e1 Joins w1,w2,G2 ; :: thesis: e1 = e2

per cases ( e2 Joins w1,w2,G2 or not e2 in the_Edges_of G2 ) by A5, Th76;

suppose e2 Joins w1,w2,G2 ; :: thesis: e1 = e2

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

end;

suppose A8: not e2 in the_Edges_of G2 ; :: thesis: e1 = e2

e2 in the_Edges_of G1 by A5, GLIB_000:def 13;
then e2 in {e} by A8, A6, XBOOLE_0:def 3;
then e2 = e by TARSKI:def 1;
then A10: e2 DJoins v1,v2,G1 by A8, Th109;

per cases ( e2 DJoins w1,w2,G1 or e2 DJoins w2,w1,G1 ) by A5, GLIB_000:16;

suppose e2 DJoins w1,w2,G1 ; :: thesis: e1 = e2

then ( (the_Source_of G1) . e2 = w1 & (the_Target_of G1) . e2 = w2 ) by GLIB_000:def 14;
then ( w1 = v1 & w2 = v2 ) by A10, GLIB_000:def 14;
hence e1 = e2 by A2, A7, CHORD:def 3; :: thesis: verum

end;

suppose e2 DJoins w2,w1,G1 ; :: thesis: e1 = e2

then ( (the_Source_of G1) . e2 = w2 & (the_Target_of G1) . e2 = w1 ) by GLIB_000:def 14;
then ( w2 = v1 & w1 = v2 ) by A10, GLIB_000:def 14;
hence e1 = e2 by A2, A7, CHORD:def 3; :: thesis: verum

end;

end;

end;

end;

end;

suppose A11: not e1 in the_Edges_of G2 ; :: thesis: e1 = e2

e1 in the_Edges_of G1 by A4, GLIB_000:def 13;
then e1 in {e} by A11, A6, XBOOLE_0:def 3;
then A12: e1 = e by TARSKI:def 1;
then A13: e1 DJoins v1,v2,G1 by A11, Th109;

per cases ( e2 Joins w1,w2,G2 or not e2 in the_Edges_of G2 ) by A5, Th76;

suppose A14: e2 Joins w1,w2,G2 ; :: thesis: e1 = e2

per cases ( e1 DJoins w1,w2,G1 or e1 DJoins w2,w1,G1 ) by A4, GLIB_000:16;

suppose e1 DJoins w1,w2,G1 ; :: thesis: e1 = e2

then ( (the_Source_of G1) . e1 = w1 & (the_Target_of G1) . e1 = w2 ) by GLIB_000:def 14;
then ( w1 = v1 & w2 = v2 ) by A13, GLIB_000:def 14;
hence e1 = e2 by A2, A14, CHORD:def 3; :: thesis: verum

end;

suppose e1 DJoins w2,w1,G1 ; :: thesis: e1 = e2

then ( (the_Source_of G1) . e1 = w2 & (the_Target_of G1) . e1 = w1 ) by GLIB_000:def 14;
then ( w2 = v1 & w1 = v2 ) by A13, GLIB_000:def 14;
hence e1 = e2 by A2, A14, CHORD:def 3; :: thesis: verum

end;

end;

end;

suppose A15: not e2 in the_Edges_of G2 ; :: thesis: e1 = e2

e2 in the_Edges_of G1 by A5, GLIB_000:def 13;
then e2 in {e} by A15, A6, XBOOLE_0:def 3;
hence e1 = e2 by A12, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

suppose ( not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ; :: thesis: G1 is non-multi

then G1 == G2 by Def11;
hence G1 is non-multi by A1, GLIB_000:89; :: thesis: verum

end;

end;