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 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 holds
e1 = e
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 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 holds
e1 = e
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 holds
e1 = e
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 implies for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 holds
e1 = e )
assume A1: not e in the_Edges_of G2 ; :: thesis: for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 holds
e1 = e
let e1, w1, w2 be object ; :: thesis: ( e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 implies e1 = e )
assume A2: ( e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 ) ; :: thesis: e1 = e
then A3: e1 in the_Edges_of G1 by GLIB_000:def 13;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, Def11;
then e1 in {e} by A3, A2, XBOOLE_0:def 3;
hence e1 = e by TARSKI:def 1; :: thesis: verum