theorem :: GLUNIR00:81

for V being non empty set
for E being Relation of V holds dom E = rng (the_Source_of (createGraph (V,E)))