let G be _Graph; :: thesis: for v, w being object holds
( [v,w] in (VertexDomRel G) ~ iff ex e being object st e DJoins w,v,G )
let v, w be object ; :: thesis: ( [v,w] in (VertexDomRel G) ~ iff ex e being object st e DJoins w,v,G )
thus ( [v,w] in (VertexDomRel G) ~ implies ex e being object st e DJoins w,v,G ) :: thesis: ( ex e being object st e DJoins w,v,G implies [v,w] in (VertexDomRel G) ~ )

proof

assume [v,w] in (VertexDomRel G) ~ ; :: thesis: ex e being object st e DJoins w,v,G
then [w,v] in VertexDomRel G by RELAT_1:def 7;
then consider e being object such that
A1: e DJoins w,v,G by Th1;
take e ; :: thesis: e DJoins w,v,G
thus e DJoins w,v,G by A1; :: thesis: verum

end;

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

proof

assume ex e being object st e DJoins w,v,G ; :: thesis: [v,w] in (VertexDomRel G) ~
then [w,v] in VertexDomRel G by Th1;
hence [v,w] in (VertexDomRel G) ~ by RELAT_1:def 7; :: thesis: verum

end;