let G be _Graph; :: thesis: the_Edges_of G = G .edgesBetween (the_Vertices_of G)
set EG = the_Edges_of G;
set SG = the_Source_of G;
set TG = the_Target_of G;

now

let x be set ; :: thesis: ( ( x in the_Edges_of G implies x in G .edgesBetween (the_Vertices_of G) ) & ( x in G .edgesBetween (the_Vertices_of G) implies x in the_Edges_of G ) )

hereby :: thesis: ( x in G .edgesBetween (the_Vertices_of G) implies x in the_Edges_of G )

assume A1: x in the_Edges_of G ; :: thesis: x in G .edgesBetween (the_Vertices_of G)
then ( (the_Source_of G) . x in the_Vertices_of G & (the_Target_of G) . x in the_Vertices_of G ) by FUNCT_2:7;
hence x in G .edgesBetween (the_Vertices_of G) by A1, Lm6; :: thesis: verum

end;

assume x in G .edgesBetween (the_Vertices_of G) ; :: thesis: x in the_Edges_of G
hence x in the_Edges_of G ; :: thesis: verum

end;

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