theorem Th2: :: GLUNIR00:2

for G being _Graph
for v, w being object holds
( [v,w] in (VertexDomRel G) ~ iff ex e being object st e DJoins w,v,G )