let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for x, y, e being object holds
( e DJoins x,y,G1 iff e DJoins x,y,G2 )
let V be set ; :: thesis: for G1 being addVertices of G2,V
for x, y, e being object holds
( e DJoins x,y,G1 iff e DJoins x,y,G2 )
let G1 be addVertices of G2,V; :: thesis: for x, y, e being object holds
( e DJoins x,y,G1 iff e DJoins x,y,G2 )
let x, y, e be object ; :: thesis: ( e DJoins x,y,G1 iff e DJoins x,y,G2 )

hereby :: thesis: ( e DJoins x,y,G2 implies e DJoins x,y,G1 )

assume e DJoins x,y,G1 ; :: thesis: e DJoins x,y,G2
then ( e in the_Edges_of G1 & (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) by GLIB_000:def 14;
then ( e in the_Edges_of G2 & (the_Source_of G2) . e = x & (the_Target_of G2) . e = y ) by Def10;
hence e DJoins x,y,G2 by GLIB_000:def 14; :: thesis: verum

end;

assume e DJoins x,y,G2 ; :: thesis: e DJoins x,y,G1
then ( e in the_Edges_of G2 & (the_Source_of G2) . e = x & (the_Target_of G2) . e = y ) by GLIB_000:def 14;
then ( e in the_Edges_of G1 & (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) by Def10;
hence e DJoins x,y,G1 by GLIB_000:def 14; :: thesis: verum