let G be _Graph; :: thesis: for v, w being object holds
( [v,w] in VertexDomRel G iff ex e being object st e DJoins v,w,G )
let v, w be object ; :: thesis: ( [v,w] in VertexDomRel G iff ex e being object st e DJoins v,w,G )
reconsider S = the_Source_of G as Relation of (the_Edges_of G),(the_Vertices_of G) ;

hereby :: thesis: ( ex e being object st e DJoins v,w,G implies [v,w] in VertexDomRel G )

assume [v,w] in VertexDomRel G ; :: thesis: ex e being object st e DJoins v,w,G
then consider e being object such that
A1: ( [v,e] in S ~ & [e,w] in the_Target_of G ) by RELAT_1:def 8;
take e = e; :: thesis: e DJoins v,w,G
[e,v] in S by A1, RELAT_1:def 7;
then A2: ( e in dom (the_Source_of G) & (the_Source_of G) . e = v ) by FUNCT_1:1;
(the_Target_of G) . e = w by A1, FUNCT_1:1;
hence e DJoins v,w,G by A2, GLIB_000:def 14; :: thesis: verum

end;

given e being object such that A3: e DJoins v,w,G ; :: thesis: [v,w] in VertexDomRel G
e in the_Edges_of G by A3, GLIB_000:def 14;
then A4: ( e in dom (the_Source_of G) & e in dom (the_Target_of G) ) by FUNCT_2:def 1;
( (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by A3, GLIB_000:def 14;
then ( [e,v] in the_Source_of G & [e,w] in the_Target_of G ) by A4, FUNCT_1:1;
then ( [v,e] in S ~ & [e,w] in the_Target_of G ) by RELAT_1:def 7;
hence [v,w] in VertexDomRel G by RELAT_1:def 8; :: thesis: verum