theorem Th17: :: GLIB_004:17

for G being real-weighted WGraph
for src being Vertex of G holds dom ((DIJK:Init src) `1) = {src}