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

now :: thesis: for x being object holds
( ( x in the_Edges_of G implies x in G .edgesInOut (the_Vertices_of G) ) & ( x in G .edgesInOut (the_Vertices_of G) implies x in the_Edges_of G ) )

let x be object ; :: thesis: ( ( x in the_Edges_of G implies x in G .edgesInOut (the_Vertices_of G) ) & ( x in G .edgesInOut (the_Vertices_of G) implies x in the_Edges_of G ) )

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

assume A1: x in the_Edges_of G ; :: thesis: x in G .edgesInOut (the_Vertices_of G)
then (the_Source_of G) . x in the_Vertices_of G by FUNCT_2:5;
hence x in G .edgesInOut (the_Vertices_of G) by A1, Th28; :: thesis: verum

end;

assume x in G .edgesInOut (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 .edgesInOut (the_Vertices_of G) by TARSKI:2; :: thesis: verum