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 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
let G1 be addEdge of G2,v1,e,v2; :: thesis: G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
thus G1 .edgesBetween (the_Vertices_of G2) = G1 .edgesBetween (the_Vertices_of G1) by Th106
.= the_Edges_of G1 by GLIB_000:34 ; :: thesis: verum