theorem Th22: :: GLIB_004:22

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