:: deftheorem defines VertexDomRel GLUNIR00:def 1 :
for G being _Graph holds VertexDomRel G = ((the_Source_of G) ~) * (the_Target_of G);