let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2)
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2)
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2)
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2) )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2)
set B = G1 .edgesBetween (the_Vertices_of G2);
for e being object holds
( e in the_Edges_of G2 iff e in G1 .edgesBetween (the_Vertices_of G2) )

proof

let e be object ; :: thesis: ( e in the_Edges_of G2 iff e in G1 .edgesBetween (the_Vertices_of G2) )

hereby :: thesis: ( e in G1 .edgesBetween (the_Vertices_of G2) implies e in the_Edges_of G2 )

assume A2: e in the_Edges_of G2 ; :: thesis: e in G1 .edgesBetween (the_Vertices_of G2)
then ( (the_Source_of G2) . e in the_Vertices_of G2 & (the_Target_of G2) . e in the_Vertices_of G2 ) by FUNCT_2:5;
then A3: ( (the_Source_of G1) . e in the_Vertices_of G2 & (the_Target_of G1) . e in the_Vertices_of G2 ) by A2, GLIB_006:def 9;
the_Edges_of G2 c= the_Edges_of G1 by GLIB_006:def 9;
hence e in G1 .edgesBetween (the_Vertices_of G2) by A3, GLIB_000:31, A2; :: thesis: verum

end;

set x = (the_Source_of G1) . e;
set y = (the_Target_of G1) . e;
assume e in G1 .edgesBetween (the_Vertices_of G2) ; :: thesis: e in the_Edges_of G2
then A4: ( e in the_Edges_of G1 & (the_Source_of G1) . e in the_Vertices_of G2 & (the_Target_of G1) . e in the_Vertices_of G2 ) by GLIB_000:31;
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G2 by A1, A4, Th49;
hence e in the_Edges_of G2 by GLIB_000:def 13; :: thesis: verum

end;

hence the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2) by TARSKI:2; :: thesis: verum