let G be _Graph; 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 ; ( [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 ( ex e being object st e DJoins v,w,G implies [v,w] in VertexDomRel G )
assume
[v,w] in VertexDomRel G
;
ex e being object st e DJoins v,w,Gthen 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;
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;
verum
end;
given e being object such that A3:
e DJoins v,w,G
; [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; verum