theorem Th1: :: GLUNIR00:1

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