theorem Th19: :: GLIB_004:19

for G being _finite real-weighted WGraph
for src being Vertex of G
for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src