theorem Th21: :: GLIB_004:21

for G being _finite real-weighted WGraph
for s being Vertex of G
for n being Nat holds card (dom (((DIJK:CompSeq s) . n) `1)) = min ((n + 1),(card (G .reachableDFrom s)))